aboutsummaryrefslogtreecommitdiff
path: root/engine/evd.ml
AgeCommit message (Expand)Author
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-14Fixing restrict regarding evar_store.Hugo Herbelin
2017-06-05Univs: fix bug #5365, generation of u+k <= v constraintsMatthieu Sozeau
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-02Don't double up on periods in anomaliesJason Gross
2017-06-01Bump year in headers.Maxime Dénès
2017-05-30Support for using type information to infer more precise evar sources.Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Fix 4.04 warningsGaetan Gilbert
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-07Merge branch 'master' into econstrPierre-Marie Pédrot
2017-03-23Ensuring static invariants about handling of pending evars in Pretyping.Pierre-Marie Pédrot
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Making Evd independent from Namegen.Pierre-Marie Pédrot
2017-02-14Moving printing code from Evd to Termops.Pierre-Marie Pédrot
2017-02-14Chasing a few unsafe constr coercions.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
2017-02-14Ltac now uses evar-based constrs.Pierre-Marie Pédrot
2017-02-01Merge branch 'v8.6'Pierre-Marie Pédrot
2017-01-23Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2017-01-22Adding a new evar source to remember the name of evars which wereHugo Herbelin
2016-12-07Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-30Fix UGraph.check_eq!Matthieu Sozeau
2016-10-30Reordering Termops w.r.t. Evd and Namegen in engine folder.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-26Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-15Fix bug #5145: Anomaly: index to an anonymous variable.Pierre-Marie Pédrot
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-08-30CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Matej Kosik
2016-08-26CLEANUP: rename "Context.Named.{to,of}_rel" functions to "Context.Named.{to,o...Matej Kosik
2016-08-25CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Contex...Matej Kosik
2016-08-25CLEANUP: removing calls of the "Context.Named.Declaration.get_value" functionMatej Kosik
2016-08-24CLEANUP: minor readability improvementsMatej Kosik
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-08-17Two protections against failures when printing evar_map.Hugo Herbelin
2016-08-10Remove unused optional "predicative" argument.Guillaume Melquiond
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-02-19Allowing to attach location to universes in UState.Pierre-Marie Pédrot
2016-02-15merging conflicts with the original "trunk__CLEANUP__Context__2" branchMatej Kosik
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:10:23 +0000