aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
Commit message (Expand)AuthorAge
* Fixing #4906 (regression in printing an error message).Gravatar Hugo Herbelin2016-07-08
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Univ: Use loc even if there are more unbound levelsGravatar Matthieu Sozeau2016-06-29
* Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
* Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Optimize the clear tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* Better algorithm for variable deambiguation in term printing.Gravatar Pierre-Marie Pédrot2016-06-23
* Document new Hint Mode option.Gravatar Matthieu Sozeau2016-06-16
* Proofview: extensions for backtracking eautoGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\
* \ Merge remote-tracking branch 'origin/pr/173' into trunkGravatar Enrico Tassi2016-06-14
|\ \
| | * Fix a typo in proofs/proofview.mli.Gravatar Cyprien Mangin2016-06-14
| | * Fix usage of Pervasives in goal selectors.Gravatar Cyprien Mangin2016-06-14
| | * Add a comment about the use of a zipper, for clarity.Gravatar Cyprien Mangin2016-06-14
| | * Add a [CList.partitioni] function.Gravatar Cyprien Mangin2016-06-14
| | * Add goal range selectors.Gravatar Cyprien Mangin2016-06-14
| |/ |/|
* | Adding a bit of documentation in the mli.Gravatar Pierre-Marie Pédrot2016-06-09
| * STM: proof block detection for bullets and { block }Gravatar Enrico Tassi2016-06-06
|/
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Normalizing the names of dynamic types to follow a typ_* scheme.Gravatar Pierre-Marie Pédrot2016-05-04
* Interpretation function can return any untyped value.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Ftactic and Geninterp to the engine folder.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving Evarutil and Proofview to engine/Gravatar Pierre-Marie Pédrot2016-03-20
* Making Proofview independent of Logic.Gravatar Pierre-Marie Pédrot2016-03-20
* Allowing to attach location to universes in UState.Gravatar Pierre-Marie Pédrot2016-02-19
* merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\
* | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-02-13
| * CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
* mergeGravatar Matej Kosik2016-01-11
|\
| * CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
* | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-01
* | Merge branch 'v8.5' into trunkGravatar Guillaume Melquiond2015-12-31
|/
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* CLEANUP: in the Reduction moduleGravatar Matej Kosik2015-12-17
* API: documenting context_chop and removing a duplicate.Gravatar Hugo Herbelin2015-12-15
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-12-11
* Fixing compilation of mli documentation.Gravatar Hugo Herbelin2015-12-05