| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-08-01 | CHANGES: [>…]. | Arnaud Spiwack | |
| 2014-08-01 | Document [> … ]. | Arnaud Spiwack | |
| 2014-08-01 | New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal. | Arnaud Spiwack | |
| 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].. ]. | |||
| 2014-08-01 | Fix English spelling -> American spelling in doc. | Arnaud Spiwack | |
| 2014-08-01 | CHANGES: [numgoals] and [guard]. | Arnaud Spiwack | |
| 2014-08-01 | Document [numgoals] and [guard]. | Arnaud Spiwack | |
| 2014-08-01 | Add [guard] tactic. | Arnaud Spiwack | |
| 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. | |||
| 2014-08-01 | Add [numgoal] to Ltac. | Arnaud Spiwack | |
| 2014-08-01 | Add primtive [num_goal] to Proofview. | Arnaud Spiwack | |
| The [num_goal] tactic counts the number of focused goals. | |||
| 2014-08-01 | Untyped terms in ltac: simplify [coerce_to_uconstr]. | Arnaud Spiwack | |
| Following advice by Hugo Herbelin. | |||
| 2014-08-01 | Remove spurious [1] in equality.ml. | Arnaud Spiwack | |
| Introduced in a4043608f | |||
| 2014-08-01 | Clean outdated comment in Proofview.Notations. | Arnaud Spiwack | |
| 2014-08-01 | Fix typo in cf04daec997. | Arnaud Spiwack | |
| 2014-08-01 | micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true) | Frédéric Besson | |
| * Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking | |||
| 2014-08-01 | Compatibility for compilation with ocaml 3.12 (at least). | Hugo Herbelin | |
| 2014-08-01 | micromega : improve efficiency/termination of type-checking | Frédéric Besson | |
| * unused terms are generalised * proof is abstract | |||
| 2014-08-01 | Continuing (incomplete) cleaning of Inductiveops. | Hugo Herbelin | |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | |
| - 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 | |||
| 2014-08-01 | Removing more tactic compatibility layer. | Pierre-Marie Pédrot | |
| 2014-08-01 | Removing some tactic compatibility layer. | Pierre-Marie Pédrot | |
| 2014-07-31 | Useless export of Instance.eqeq. We hashcons everything before calling this | Pierre-Marie Pédrot | |
| function, so plain pointer equality is sufficient. | |||
| 2014-07-31 | Making the error message about bullets more precise. | Pierre Courtieu | |
| Suggests in some cases the right bullet to use. | |||
| 2014-07-31 | Removing the call to Weak.get_copy in hashsets. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-07-31 | micromega : refification recognises @eq T for T convertible with Z or R | Frédéric Besson | |
| 2014-07-31 | Typos. | Hugo Herbelin | |
| 2014-07-31 | Finish fixes on notations and primitive projections, add test-suite files ↵ | Matthieu Sozeau | |
| for closed bugs | |||
| 2014-07-31 | Consistent pretty-printing of primitive projections and their expanded forms. | Matthieu Sozeau | |
| 2014-07-31 | Add an option to solve typeclass goals generated by apply which can't be | Matthieu Sozeau | |
| catched otherwise due to the discrepancy between evars and metas. | |||
| 2014-07-31 | Adding a generalized version of fold_Equal to FMapFacts. | Pierre Courtieu | |
| 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. | |||
| 2014-07-31 | Optimize check of new subterm relation on match. | Maxime Dénès | |
| 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. | |||
| 2014-07-31 | Improve intersection of regular trees. | Maxime Dénès | |
| For better efficiency, we try to preserve the shape of mutually recursive trees. | |||
| 2014-07-31 | Fix dynamic computation of recargs for mutual inductives. | Maxime Dénès | |
| Used by the new guard criterion compatible with type isomorphisms. | |||
| 2014-07-30 | Add test-suite file for bug #3439. | Matthieu Sozeau | |
| 2014-07-30 | Avoid hconsing instances during appends and conversions from/to arrays. | Matthieu Sozeau | |
| 2014-07-30 | Fix discrimination net which was not recognizing primitive projections. | Matthieu Sozeau | |
| 2014-07-30 | Avoid introducing additional universes when doing pruning in evarsolve. | Matthieu Sozeau | |
| 2014-07-29 | CHANGES: untyped terms in tactics | Arnaud Spiwack | |
| 2014-07-29 | Document untyped terms in tactics. | Arnaud Spiwack | |
| 2014-07-29 | Small refactoring in Ltac parsing rules. | Arnaud Spiwack | |
| 2014-07-29 | Allow [uconstr:c] as argument of a tactic. | Arnaud Spiwack | |
| 2014-07-29 | Untyped terms in tactic: add the possibility to use a typed term inside an ↵ | Arnaud Spiwack | |
| untyped term. | |||
| 2014-07-29 | Untyped terms in tactic: function [type_term c] to give a typed version of [c]. | Arnaud Spiwack | |
| 2014-07-29 | Untyped term in tactics: add an grammar entry to construct them. | Arnaud Spiwack | |
| The syntax is uconstr:term. | |||
| 2014-07-29 | Add a type of untyped term to Ltac's value. | Arnaud Spiwack | |
| 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. | |||
| 2014-07-29 | Clean up obsolete comment. | Arnaud Spiwack | |
| 2014-07-29 | Add test-suite file for bug 3454. | Matthieu Sozeau | |
| 2014-07-29 | Rework code for refolding projections in whd_state/whd_simpl to allow Arguments | Matthieu Sozeau | |
| Specifications indicating that the record object must be a constructor. Fixes bug #3432. | |||
| 2014-07-29 | Fix eta-conversion code which was failing in nested cases. Fixes bug #3429. | Matthieu Sozeau | |
| 2014-07-29 | Add test-suite file for bug #3453 | Matthieu Sozeau | |
| 2014-07-29 | Fix bug #3453, not recognizing primitive projections in Coercion declarations. | Matthieu Sozeau | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |