Permalink
Commits on Nov 2, 2013
  1. Fix set: nf_evar prior to tactic interpretation.

    Noticed in CoRN
    committed Oct 31, 2013
  2. Plug back infoH.

    committed Oct 31, 2013
  3. Plugs back external tactics.

    committed Oct 31, 2013
  4. Fix the log of debug auto.

    committed Oct 31, 2013
  5. Update comments.

    committed Oct 31, 2013
  6. Doc: solve the bad interaction between Declare Implicit Tactic and re…

    …fine.
    
    An implicit tactic was declared and made refine fail (trying to solve the open goals of the refined term resulted in an error). There was no way to remove the implicit tactic (it isn't managed by an option so isn't removed by Reset Initial). I added the option under the name Clear Implicit Tactic.
    committed Oct 31, 2013
  7. Documentation for the backtracking features.

    This required some reorganisation of the documentation of existing tacticals. I hope the result is consistent.
    committed Oct 31, 2013
  8. Fix destruct: nf_evar prior to tactic interpretation.

    Noticed in CoRN
    committed Oct 31, 2013
  9. Fix congruence: normalise hypotheses with respect to evars.

    Detected in CompCert.
    committed Oct 31, 2013
  10. push_rel_context: do not rename section variables.

    Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect)
    committed Oct 30, 2013
  11. Refine now does iota reduction in addition to beta.

    Restores more compatibility with the earlier implementation of refine. Needed in ssreflect.
    committed Oct 30, 2013
  12. Fix compilation of pattern matching wrt variables: alias.

    Aliases (as clause) are a bit tricky.
    
    In Goal True,
    
    refine match 0 with
    | S n as p => _
    | _ => I
    end
    
    Must produce the goal
    
    n:nat, p := S n : nat |- True
    
    However, in the deep branches:
    
    refine match 0 with
    | S (S n as p) => _
    | _ => I
    end
    
    The alias is used to give a name to the variable of the first S :
    
    p:nat, n:nat |- True
    
    Before this patch, the goal would be
    
    p:nat, n:nat, p:=p : nat |- True
    
    Alias was used both to name the variable of the first S and to alias it.
    committed Oct 28, 2013
  13. Fix the compilation of pattern matching wrt to variables.

    Compilation of pattern-matching used to systematically introduce a dummy alias x:=x in the typing environment for each variable x in the patterns (except for purely variable patterns which correctly alias the term being matched). This interfered badly with the new refine implementation.
    
    To correct this I changed the "all variables" case of pattern-matching compilation to check whether the term currently being matched is a term introduced by the user or a subterm which is necessarily a variable. In the latter case, no alias is introduced.
    committed Oct 24, 2013
  14. Refine: Tactics.New.refine does beta-reduction.

    Previously I had wrapped Tactics.New.refine with extra
    beta-reduction in extratactics.ml4, that is, only for Ltac.
    Ocaml plugins saw the version without reduction.
    committed Oct 21, 2013
  15. Adds a tactic give_up.

    Gives up on the focused goals. Shows an unsafe status. Unlike the admit tactic, the proof cannot be closed until the users goes back and solves these goals.
    committed Oct 17, 2013
  16. A tactic shelve_unifiable.

    Puts on the shelf every goals under focus on which other goals under focus
    depend. Useful when we want to solve these goals by unification (as in a
    first order proof search procedure, for instance).
    
    Also meant to be able to recover approximately the semantics of the old
    refine with the new implementation (use refine t; shelve_unifiable).
    
    TODO: bug dans l'example de shelve_unifiable
    committed Oct 25, 2013
  17. Made multiple-goal tactic work after all: .

    Internalization was done relative to a goal. It doesn't make sense in the
    case of all:. When we make a tactic with all: the environment for
    internalization is taken to be the global environment.
    committed Oct 16, 2013
  18. Make multiple-goal tactics possible after a tclTHEN.

    Tacinterp used to interprete every tactics inside a goal, making
    multiple-goal tactics act on a single goal anyway.
    
    Uses a simple heuristic to decide when a goal is not needed.
    committed Oct 16, 2013
  19. Corrects a bug on Proofview.Goal.enter whereby sigmas were captured a…

    …nd used at the wrong time.
    
    The bug was masked by the fact that Tacinterp uses many superfluous Proofview.Goal.enter, it so happens that the tactic
    Proofview.Goal.enter (fun _ -> Proofview.Goal.enter fun gl -> t))
    had the correct semantics!
    committed Oct 16, 2013
  20. Adds a shelve tactic.

    The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.
    committed Oct 17, 2013
  21. bootstrap/Monad.v: implements the writer monad in continuation passin…

    …g style.
    
    Benefits: fewer pair constructed/destructed especially in split.
    Potential costs: plus and zero now have closures with 11 arguments.
    committed Oct 15, 2013
  22. bootstrap/Monad.v: implements the environment monad in continuation p…

    …assing style.
    
    Benefits: the underlying monads are not referenced in the "current" primitive.
    Potential costs: some extracted functions now have 9 arguments, Ocaml may not be good at handling these. The split primitive, which is called often, now builds one extra closure.
    committed Oct 15, 2013
  23. Factors the lifting of environment and writer monads in bootstrap/Mon…

    …ad.v
    
    Takes a few extra lines but is probably more robust to future changes.
    Doesn't change the extracted code.
    committed Oct 15, 2013
  24. Adds an experimental exactly_once tactical.

    exactly_once t, will have a success if t has exactly once success.
    
    There are a few caveats:
    - The underlying effects of t may happen in an unpredictable order (hence it may be wise to use it only with "pure" tactics)
    - The second success of a tactic is conditional on the exception thrown. In Ltac it doesn't show, but in the underlying code, the tactical also expects the exception you want to use to produce the second success.
    committed May 22, 2013
  25. Made Proofview.Goal.hyps a named_context.

    There was really no point in having it be a named_context val. The tactics are not going to access the vm cache. Only vm_compute will.
    committed Mar 15, 2013
  26. Refine does beta-reductions.

    To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta.
    committed Mar 13, 2013
  27. A dedicated view type for Proofview_gen.split.

    It doesn't seem to affect performances. But the generated code is slightly cleaner.
    committed Mar 11, 2013
  28. Adds a tactical once.

    [once t] does just as [t] but has exactly one success it [t] has at least one success.
    committed Mar 5, 2013