Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | * | | | | | | | Use msg_info for LtacProf | 2017-12-11 | ||
| | | | * | | | | | | | Allow LtacProf tactics to be called | 2017-12-11 | ||
| | | | | |_|_|/ / / | | | | |/| | | | | | ||||
| | | | | | * | | | | Catch errors while coercing 'and' intro patterns | 2017-12-11 | ||
| | | | | |/ / / / | | | | |/| | | | | ||||
* | | | / | | | | | [proof] Embed evar_map in RefinerError exception. | 2017-12-11 | ||
| |_|_|/ / / / / |/| | | | | | | | ||||
| | * | | | | | | Remove deprecated appcontext and corresponding documentation. | 2017-12-11 | ||
| | * | | | | | | Remove deprecated option Tactic Compat Context. | 2017-12-11 | ||
| |/ / / / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #6324: Fix #6323: stronger restrict universe context vs abstract. | 2017-12-11 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #1150: [stm] Remove all but one use of VtUnknown. | 2017-12-11 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6338: Remove up-to-conversion term matching | 2017-12-11 | ||
|\ \ \ \ \ \ \ \ \ | |_|_|_|/ / / / / |/| | | | | | | | | ||||
| | | | * | | | | | [lib] Rename Profile to CProfile | 2017-12-09 | ||
| |_|_|/ / / / / |/| | | | | | | | ||||
| | * | | | | | | [stm] Remove all but one use of VtUnknown. | 2017-12-09 | ||
| |/ / / / / / |/| | | | | | | ||||
* | | | | | | | Merge PR #6158: Allows a level in the raw and glob printers | 2017-12-08 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #6322: Fix #6286 (non stability of micromega csdp cache rebuilding) | 2017-12-07 | ||
|\ \ \ \ \ \ \ \ | ||||
| | | * | | | | | | Getting rid of pf_is_matching in Funind. | 2017-12-06 | ||
| |_|/ / / / / / |/| | | | | | | | ||||
| | | | | | * | | issue deprecation warning for "Ocaml" | 2017-12-06 | ||
| | | * | | | | | Fix #6323: stronger restrict universe context vs abstract. | 2017-12-06 | ||
| |_|/ / / / / |/| | | | | | | ||||
| * | | | | | | Replacing Hashtbl.add by Hashtbl.replace in micromega cache building. | 2017-12-05 | ||
| | | | | * | | use \ocaml macro in Extraction chapter; accept OCaml in Extraction Language | 2017-12-05 | ||
| |_|_|_|/ / |/| | | | | | ||||
* | | | | | | Merge PR #890: Global universe declarations | 2017-12-05 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212 | 2017-12-05 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #6210: More complete not-fully-applied error messages, #6145 | 2017-12-05 | ||
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | ||||
| | | * | | | | | Proper nametab handling of global universe names | 2017-12-01 | ||
| |_|/ / / / / |/| | | | | | | ||||
* | | | | | | | Remove "obsolete_locality" and fix STM vernac classification. | 2017-11-29 | ||
| |_|_|_|/ / |/| | | | | | ||||
| * | | | | | more complete not-fully-applied error messages, #6145 | 2017-11-28 | ||
| | | | | * | Make the micromega extraction check a regular output test. | 2017-11-28 | ||
| |_|_|_|/ |/| | | | | ||||
* | | | | | Merge PR #1033: Universe binder improvements | 2017-11-28 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #6248: [api] Remove aliases of `Evar.t` | 2017-11-28 | ||
|\ \ \ \ \ \ | ||||
| | | | * | | | allow :: and , as infix ops | 2017-11-27 | ||
| * | | | | | | [api] Remove aliases of `Evar.t` | 2017-11-26 | ||
* | | | | | | | Use Evarutil.has_undefined_evars for tactic has_evar. | 2017-11-24 | ||
|/ / / / / / | ||||
| * | | | | | Use Entries.constant_universes_entry more. | 2017-11-24 | ||
| * | | | | | When declaring constants/inductives use ContextSet if monomorphic. | 2017-11-24 | ||
| * | | | | | Stop exposing UState.universe_context and its Evd wrapper. | 2017-11-24 | ||
| * | | | | | Separate checking univ_decls and obtaining universe binder names. | 2017-11-24 | ||
|/ / / / / | ||||
| | | * | | Extending further PR#6047 (system to register printers for Ltac values). | 2017-11-24 | ||
| | | * | | Printing again "intros **" as "intros" by default. | 2017-11-24 | ||
| |_|/ / |/| | | | ||||
* | | | | Merge PR #6205: Fixing a 8.7 regression of ring_simplify in ArithRing | 2017-11-24 | ||
|\ \ \ \ | ||||
* \ \ \ \ | Merge PR #486: Make some functions on terms more robust w.r.t new term constr... | 2017-11-24 | ||
|\ \ \ \ \ | ||||
* \ \ \ \ \ | Merge PR #876: In omega or romega, recognizing Z and nat modulo conversion | 2017-11-24 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #6197: [plugin] Remove LocalityFixme über hack. | 2017-11-24 | ||
|\ \ \ \ \ \ \ | ||||
| | | * | | | | | Make some functions on terms more robust w.r.t new term constructs. | 2017-11-23 | ||
* | | | | | | | | Merge PR #6186: [api] Miscellaneous consolidation. | 2017-11-23 | ||
|\ \ \ \ \ \ \ \ | |_|_|/ / / / / |/| | | | | | | | ||||
| | | * | | | | | Recognizing Z in romega up to conversion. | 2017-11-23 | ||
| | | * | | | | | Using is_conv rather than eq_constr to find `nat` or `Z` in omega. | 2017-11-23 | ||
| |_|/ / / / / |/| | | | | | | ||||
| | | * | | | | Fixing a 8.7 regression of ring_simplify in ArithRing. | 2017-11-23 | ||
| |_|/ / / / |/| | | | | | ||||
* | | | | | | Merge PR #6192: Fix #5790: make Hint Resolve <- respect univ polymorphism flag. | 2017-11-23 | ||
|\ \ \ \ \ \ | ||||
| | | * | | | | [plugin] Remove LocalityFixme über hack. | 2017-11-22 | ||
| |_|/ / / / |/| | | | | | ||||
| | | | * | | allow whitespace around infix op | 2017-11-22 | ||
| | | | * | | use OCaml criteria for infix ops, #6212 | 2017-11-22 | ||
| |_|_|/ / |/| | | | | ||||
| | * | | | [api] Deprecate Term destructors, move to Constr | 2017-11-22 |