aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* CHANGES: [>…].Gravatar Arnaud Spiwack2014-08-01
|
* Document [> … ].Gravatar Arnaud Spiwack2014-08-01
|
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | Differs from the usual t;[t1…tn] in two ways: * It can be used without a preceding tactic * It counts every focused subgoal, rather than considering independently the goals generated by the application of the preceding tactic on individual goals. In other words t;[t1…tn] is [> t;[>t1…tn].. ].
* Fix English spelling -> American spelling in doc.Gravatar Arnaud Spiwack2014-08-01
|
* CHANGES: [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
|
* Document [numgoals] and [guard].Gravatar Arnaud Spiwack2014-08-01
|
* Add [guard] tactic.Gravatar Arnaud Spiwack2014-08-01
| | | | | | | | The [guard] tactic accepts simple tests (on integers) as argument, succeeds if the test passes and fails if the test fails. Together with [numgoal] can be used to fork on the number of goals of a tactic. The syntax is not very robust (in particular [guard n<=1] is correct but not [guard (n<=1)]). Maybe tests should be moved to the general parser to allow for more flexibility.
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
|
* Add primtive [num_goal] to Proofview.Gravatar Arnaud Spiwack2014-08-01
| | | | The [num_goal] tactic counts the number of focused goals.
* Untyped terms in ltac: simplify [coerce_to_uconstr].Gravatar Arnaud Spiwack2014-08-01
| | | | Following advice by Hugo Herbelin.
* Remove spurious [1] in equality.ml.Gravatar Arnaud Spiwack2014-08-01
| | | | Introduced in a4043608f
* Clean outdated comment in Proofview.Notations.Gravatar Arnaud Spiwack2014-08-01
|
* Fix typo in cf04daec997.Gravatar Arnaud Spiwack2014-08-01
|
* micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)Gravatar Frédéric Besson2014-08-01
| | | | * Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
* Compatibility for compilation with ocaml 3.12 (at least).Gravatar Hugo Herbelin2014-08-01
|
* micromega : improve efficiency/termination of type-checkingGravatar Frédéric Besson2014-08-01
| | | | | * unused terms are generalised * proof is abstract
* Continuing (incomplete) cleaning of Inductiveops.Gravatar Hugo Herbelin2014-08-01
|
* A tentative uniform naming policy in module Inductiveops.Gravatar Hugo Herbelin2014-08-01
| | | | | | | | | | | | - realargs: refers either to the indices of an inductive, or to the proper args of a constructor - params: refers to parameters (which are common to inductive and constructors) - allargs = params + realargs - realdecls: refers to the defining context of indices or proper args of a constructor (it includes letins) - paramdecls: refers to the defining context of params (it includes letins) - alldecls = paramdecls + realdecls
* Removing more tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
|
* Useless export of Instance.eqeq. We hashcons everything before calling thisGravatar Pierre-Marie Pédrot2014-07-31
| | | | function, so plain pointer equality is sufficient.
* Making the error message about bullets more precise.Gravatar Pierre Courtieu2014-07-31
| | | | Suggests in some cases the right bullet to use.
* Removing the call to Weak.get_copy in hashsets.Gravatar Pierre-Marie Pédrot2014-07-31
| | | | | | | | | | | | The rationale for its use comes from OCaml weak maps, and is justified by the fact that Weak.get may prevent its return value to be collected by the GC during the next slice even though nobody points to it. In our case, this is vastly irrelevant because hashconsed values are not expected to be collected whatsoever (save for exceptional cases). But Weak.get_copy is rather costly actually, at least strictly more than the plain Weak.get. Experimentally, I observe diminution of compilation time and even diminution of memory consumption (!) after this patch, so I assume it is a net gain.
* micromega : refification recognises @eq T for T convertible with Z or RGravatar Frédéric Besson2014-07-31
|
* Typos.Gravatar Hugo Herbelin2014-07-31
|
* Finish fixes on notations and primitive projections, add test-suite files ↵Gravatar Matthieu Sozeau2014-07-31
| | | | for closed bugs
* Consistent pretty-printing of primitive projections and their expanded forms.Gravatar Matthieu Sozeau2014-07-31
|
* Add an option to solve typeclass goals generated by apply which can't beGravatar Matthieu Sozeau2014-07-31
| | | | catched otherwise due to the discrepancy between evars and metas.
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
| | | | | | | This commit should be refactored by Pierre L. if he thinks this should replace the previous version of fold_Equal, for now it is a different lemma fold_Equal2. Same for the Section addded to SetoiList, it should maybe replace the previous one.
* Optimize check of new subterm relation on match.Gravatar Maxime Dénès2014-07-31
| | | | | | | If the return predicate is not dependent, we avoid dynamically regenerating the regular tree of the corresponding inductive type. This includes the commutative cut rule. Should solve some performance issues observed in Compcert and Paco at Qed time.
* Improve intersection of regular trees.Gravatar Maxime Dénès2014-07-31
| | | | | For better efficiency, we try to preserve the shape of mutually recursive trees.
* Fix dynamic computation of recargs for mutual inductives.Gravatar Maxime Dénès2014-07-31
| | | | Used by the new guard criterion compatible with type isomorphisms.
* Add test-suite file for bug #3439.Gravatar Matthieu Sozeau2014-07-30
|
* Avoid hconsing instances during appends and conversions from/to arrays.Gravatar Matthieu Sozeau2014-07-30
|
* Fix discrimination net which was not recognizing primitive projections.Gravatar Matthieu Sozeau2014-07-30
|
* Avoid introducing additional universes when doing pruning in evarsolve.Gravatar Matthieu Sozeau2014-07-30
|
* CHANGES: untyped terms in tacticsGravatar Arnaud Spiwack2014-07-29
|
* Document untyped terms in tactics.Gravatar Arnaud Spiwack2014-07-29
|
* Small refactoring in Ltac parsing rules.Gravatar Arnaud Spiwack2014-07-29
|
* Allow [uconstr:c] as argument of a tactic.Gravatar Arnaud Spiwack2014-07-29
|
* Untyped terms in tactic: add the possibility to use a typed term inside an ↵Gravatar Arnaud Spiwack2014-07-29
| | | | untyped term.
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
|
* Untyped term in tactics: add an grammar entry to construct them.Gravatar Arnaud Spiwack2014-07-29
| | | | The syntax is uconstr:term.
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
| | | | | | It is meant to avoid intermediary retyping when a term is built in Ltac. See #3218. The implementation makes a small modification in Constrintern: now the main internalisation function can take an extra substitution from Ltac variables to glob_constr and will apply the substitution during the internalisation.
* Clean up obsolete comment.Gravatar Arnaud Spiwack2014-07-29
|
* Add test-suite file for bug 3454.Gravatar Matthieu Sozeau2014-07-29
|
* Rework code for refolding projections in whd_state/whd_simpl to allow ArgumentsGravatar Matthieu Sozeau2014-07-29
| | | | Specifications indicating that the record object must be a constructor. Fixes bug #3432.
* Fix eta-conversion code which was failing in nested cases. Fixes bug #3429.Gravatar Matthieu Sozeau2014-07-29
|
* Add test-suite file for bug #3453Gravatar Matthieu Sozeau2014-07-29
|
* Fix bug #3453, not recognizing primitive projections in Coercion declarations.Gravatar Matthieu Sozeau2014-07-29
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 18:48:12 +0000