aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Removing tactic compatibility layer in congruence.Gravatar Pierre-Marie Pédrot2017-04-24
* Removing tactic compatibility layer in Micromega.Gravatar Pierre-Marie Pédrot2017-04-24
* Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
* Removing trivial compatibility layer in refl_omega.Gravatar Pierre-Marie Pédrot2017-04-24
* Porting omega to the new tactic API.Gravatar Pierre-Marie Pédrot2017-04-24
* Removing trivial compatibility layer in omega.Gravatar Pierre-Marie Pédrot2017-04-24
* Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Maxime Dénès2017-04-24
|\
* \ Merge PR#565: Remove VernacErrorGravatar Maxime Dénès2017-04-24
|\ \
* \ \ Merge branch v8.6 into trunkGravatar Hugo Herbelin2017-04-22
|\ \ \
| | * | Remove VernacErrorGravatar Gaetan Gilbert2017-04-21
| |/ / |/| |
| | * [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
| |/ |/|
* | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \
* | | Silence a few OCaml warnings.Gravatar Guillaume Melquiond2017-04-13
* | | Merge PR#441: Port Toplevel to the Stm APIGravatar Maxime Dénès2017-04-12
|\ \ \
| * | | [stm] Remove edit_id.Gravatar Emilio Jesus Gallego Arias2017-04-12
* | | | Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...Gravatar Maxime Dénès2017-04-12
|\ \ \ \
* \ \ \ \ Merge PR#532: Clean Nsatz implementation.Gravatar Maxime Dénès2017-04-11
|\ \ \ \ \
* \ \ \ \ \ Merge PR#379: Introducing evar-insensitive constrsGravatar Maxime Dénès2017-04-11
|\ \ \ \ \ \ | |_|_|/ / / |/| | | | |
| | * | | | Fix an algorithmic issue in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| | * | | | Academic prescriptivism strikes back: down with baroque programming in Nsatz.Gravatar Pierre-Marie Pédrot2017-04-09
| |/ / / / |/| | | |
| * | | | Fix an unhandled exception in Omega.Gravatar Pierre-Marie Pédrot2017-04-07
| * | | | Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
| |\ \ \ \
* | | | | | [camlpX] Remove camlp4 compat layer.Gravatar Emilio Jesus Gallego Arias2017-04-07
| |/ / / / |/| | | |
* | | | | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \ \ \ \
* \ \ \ \ \ Merge PR#508: Optimize pending evarsGravatar Maxime Dénès2017-04-06
|\ \ \ \ \ \
| | | * | | | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
| | | | | | * end of correction of bug 4306Gravatar Julien Forest2017-04-04
| | | | | | * Bad correction in previous commitGravatar Julien Forest2017-04-04
| | | | | | * Solving first problem in bug #4306. TO DO : solve the let in problemGravatar Julien Forest2017-04-04
| | | | | |/
| | | * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
| | | |\ \ \ | |_|_|/ / / |/| | | | |
* | | | | | Merge PR#417: No cast surgery in let inGravatar Maxime Dénès2017-04-03
|\ \ \ \ \ \
| | | | * | | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | | | | | | Declaring ltac plugin, so that static linking works.Gravatar Hugo Herbelin2017-04-01
| | | | * | | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | * | | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| | | | |\ \ \ | |_|_|_|/ / / |/| | | | | |
| * | | | | | Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| * | | | | | Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | | | | Renaming local_binder into local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| * | | | | | "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
|/ / / / / /
| | | | * / Improving the API of constrexpr_ops.mli.Gravatar Hugo Herbelin2017-03-23
| |_|_|/ / |/| | | |
* | | | | Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."Gravatar Maxime Dénès2017-03-23
* | | | | Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ | | |_|_|/ | |/| | |
| * | | | Merge PR#495: funind: Ignore missing info for current functionGravatar Maxime Dénès2017-03-23
| |\ \ \ \
| | | * | | Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
| | | * | | Ensuring static invariants about handling of pending evars in Pretyping.Gravatar Pierre-Marie Pédrot2017-03-23
| * | | | | Add empty Extraction.v and FunInd.v to prepare landing of PR#220.Gravatar Maxime Dénès2017-03-23
* | | | | | Mark ring morphisms as opaque.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Fix broken evaluation strategies for ring and field.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Remove duplicate lemmas.Gravatar Guillaume Melquiond2017-03-22
| |_|/ / / |/| | | |