| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-03-25 | Moving back some tactics not essentially related to Ltac into the tactics/ ↵ | Pierre-Marie Pédrot | |
| folder. | |||
| 2016-03-25 | Moving Autorewrite back to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Autorewrite independent from Ltac. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eqdecide to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Making Eqdecide independent of Extratactics. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving Eauto and Class_tactics to tactics/. | Pierre-Marie Pédrot | |
| 2016-03-25 | Moving type_uconstr to Pretyping. | Pierre-Marie Pédrot | |
| 2016-03-25 | Test suite file for a bug in BigQ arithmetic fixed a while ago. | Maxime Dénès | |
| 2016-03-25 | Test suite file for a bug in int31 arithmetic fixed a while ago. | Maxime Dénès | |
| 2016-03-25 | Remove int64 emulation in bytecode interpreter. | Maxime Dénès | |
| We now assume an int64 type is provided by the C compiler. The emulation file was already not compiling, so it is probably not used even on exotic architectures. These files come from OCaml, where they are no longer used either. | |||
| 2016-03-25 | Fix a bug in Program coercion code | Matthieu Sozeau | |
| It was not accounting for the universe constraints generated by applications of the coercion. | |||
| 2016-03-24 | Fix handling of arity of definitional classes. | Matthieu Sozeau | |
| The user-provided sort was ignored for them. | |||
| 2016-03-24 | use printf instead of sequenced calls to print. | Gregory Malecha | |
| 2016-03-24 | add a .merlin target to the makefile | Gregory Malecha | |
| 2016-03-23 | Revert "refine: do check all unif problems are solved (Close: #4415, #4532)" | Enrico Tassi | |
| This fix is too restrictive. Still, opening a goal for an evar with a pending conv_pb is unsafe since the user may prove (instantiate it) in a way not compatible with the conv_pb. Assigning an evar, in its lowest level API, should enforce that all related conv_pbs are satisfied by the instance. This also poses a UI problem, since there is not way to see these conv_pbs. One could print a goal and say: look, the proof term you give must validate this equation... Given that the good fix is not obvious, we revert! This reverts commit a0e792236c9666df1069753f8f807c12f713dcfb. | |||
| 2016-03-23 | refine: do check all unif problems are solved (Close: #4415, #4532) | Enrico Tassi | |
| This fixes a class of bugs like refine foo; tactic. where tactic fails (by resuming the remaining, unsolvable, problems) while in 8.4 refine was failing. It is not clear to us (Maxime and myself) if we should call consider_remaining_unif_problems instead of check_problems_are_solved. | |||
| 2016-03-22 | A patch renaming equal into eq in the module dealing with | Hugo Herbelin | |
| hash-consing, so as to avoid having too many kinds of equalities with same name. | |||
| 2016-03-22 | Adding eq/compare/hash for syntactic view at | Hugo Herbelin | |
| constant/inductive/constructor kernel_name pairs rather than viewing them from only the user or canonical part. Hopefully more uniformity in Constr.hasheq (using systematically == on subterms). A semantic change: Cooking now indexing again on full pairs of kernel names rather than only on the canonical names, so as to preserve user name. Also, in pair of kernel names, ensuring the compact representation is used as soon as both names are the same. | |||
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-21 | Moving the last parts of the Ltac engine to hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacsubst to hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Relying on generic arguments to represent Extern hints. | Pierre-Marie Pédrot | |
| 2016-03-20 | Adding a new Ltac generic argument for forced tactics returing unit. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacenv to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic_debug to Hightactic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the lowest parts of pretyping/ (Evarutil & Proofview) to engine/. | Pierre-Marie Pédrot | |
| Some functions exported by Evarutil essentially used by the unification engine were moved to a new file Evardefine. Their presence in Evarutil was not making much sense. Moreover, the Refine module of the Proofview file was turned into a proper file in pretyping/. This is because this part of the code was relying on the typing primitives from Pretyping. | |||
| 2016-03-20 | Documenting changes. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Evarutil and Proofview to engine/ | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Evarutil independent from Reductionops. | Pierre-Marie Pédrot | |
| 2016-03-20 | Splitting Evarutil in two distinct files. | Pierre-Marie Pédrot | |
| Some parts of Evarutils were related to the management of evars under constraints. We put them in the Evardefine file. | |||
| 2016-03-20 | Pushing Proofview further down the dependency alley. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Proofview to pretyping/. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Refine to its proper module. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent of Logic. | Pierre-Marie Pédrot | |
| 2016-03-20 | Making Proofview independent from Goal. | Pierre-Marie Pédrot | |
| 2016-03-20 | Extruding the code for the Existential command from Proofview. | Pierre-Marie Pédrot | |
| 2016-03-20 | Merge branch 'v8.5' | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing the classification of Tactic Notation. | Pierre-Marie Pédrot | |
| 2016-03-20 | Fixing bug #4630: Some tactics are 20x slower in 8.5 than 8.4. | Pierre-Marie Pédrot | |
| The interpretation of arguments of tactic notations were normalizing the goal beforehand, which incurred an important time penalty. We now do this argumentwise which allows to save time in frequent cases, notably tactic arguments. | |||
| 2016-03-20 | Moving most of Ltac code to Hightactics. | Pierre-Marie Pédrot | |
| This is a major step towards the pluginification of Ltac. The one important file that is out of reach for now is Tacsubst, as it is used in an intricate way to handle amongst other things auto hints. | |||
| 2016-03-20 | Moving Tacintern to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the Ltac definition command to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving the tactic related code from Metasyntax to a new file. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Print Ltac to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tactic Notation to an EXTEND based command. | Pierre-Marie Pédrot | |
| 2016-03-20 | Moving Tacinterp to Hightactics. | Pierre-Marie Pédrot | |
| 2016-03-19 | Moving the use of Tactic_option from Obligations to G_obligations. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Fixing compilation with old versions of CAMLP5. | Pierre-Marie Pédrot | |
| 2016-03-19 | Removing dead code in Genarg. | Pierre-Marie Pédrot | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |