| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 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 | |
| 2014-07-29 | Fix treatment of notations containing applications of projections (fixes bug ↵ | Matthieu Sozeau | |
| #3454). | |||
| 2014-07-29 | STM: print goals with no duplicates | Enrico Tassi | |
| 2014-07-29 | Pp: only one default feedback id | Enrico Tassi | |
| 2014-07-29 | Pp compiles after feedback | Enrico Tassi | |
| 2014-07-28 | CPS-style tactic matching. We use the tactic monad as the target of the CPS. | Pierre-Marie Pédrot | |
| This allows for tail-rec calls, prevents unwanted capture of closures and results in an overall more efficient evaluation. | |||
| 2014-07-28 | Adding a tclBREAK primitive to the tactic monad. | Pierre-Marie Pédrot | |
| 2014-07-27 | Code cleaning in Tacenv. | Pierre-Marie Pédrot | |
| 2014-07-27 | Qualified ML tactic names. The plugin name is used to discriminate | Pierre-Marie Pédrot | |
| potentially conflicting tactics names from different plugins. | |||
| 2014-07-25 | Removing dead code relative to or_metaid. | Pierre-Marie Pédrot | |
| 2014-07-25 | CHANGES: cycle and swap. | Arnaud Spiwack | |
| 2014-07-25 | Document swap tactic. | Arnaud Spiwack | |
| 2014-07-25 | Document cycle tactic. | Arnaud Spiwack | |
| 2014-07-25 | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack | |
| If [i] or [j] is negative goals are counted from the end. | |||
| 2014-07-25 | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack | |
| [cycle 1] puts the first goal last, [cycle -1] puts the last goal first, [cycle n] is like [do n cycle 1], [cycle -n] is like [do n cycle -1]. | |||
| 2014-07-25 | A slightly more fine grained way to check whether a TACTIC EXTEND is global ↵ | Arnaud Spiwack | |
| or local to goals. Checks if the arguments need anything from the goal by looking at their tags, if not, the tactic is global. | |||
| 2014-07-25 | CHANGES: yellow in Coqide. | Arnaud Spiwack | |
| 2014-07-25 | CHANGE: add Derive. | Arnaud Spiwack | |
| 2014-07-25 | CHANGE: document the features of the new tactic engine. | Arnaud Spiwack | |
| 2014-07-25 | Update the documentation of Ltac's ";" and ";[…]" to reflect the new ↵ | Arnaud Spiwack | |
| multi-goal semantics of tactics. | |||
| 2014-07-25 | Warns about inconsistency of generated name in evars and goals. | Arnaud Spiwack | |
| See bug #1041 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |