| Commit message (Expand) | Author | Age |
... | |
* | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau | 2014-05-06 |
* | Fix interface for template polymorphism, cleaning up code in all typing algor... | Matthieu Sozeau | 2014-05-06 |
* | Properly reinstate old-style polymorphism in the kernel and pretyping/retyping. | Matthieu Sozeau | 2014-05-06 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Fixing bug #3228 (fixing precedence of ltac variables over variables in env). | Hugo Herbelin | 2014-04-05 |
* | TC: honor the use_typeclasses flag in pretyping | Enrico Tassi | 2014-02-12 |
* | Support for evars and metas in native compiler. | Maxime Dénès | 2013-12-30 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | Get rid of the uses of deprecated OCaml elements (still remaining compatible ... | xclerc | 2013-09-19 |
* | Removing useless casts between arrays and lists. | ppedrot | 2013-08-04 |
* | Using the whole tactic environment while Pretyping. | ppedrot | 2013-06-24 |
* | Generalizing the use of maps instead of lists in the interpretation | ppedrot | 2013-06-22 |
* | A uniformization step around understand_* and interp_* functions. | herbelin | 2013-05-09 |
* | Merging Context and Sign. | ppedrot | 2013-04-29 |
* | Splitting Term into five unrelated interfaces: | ppedrot | 2013-04-29 |
* | Avoid a few overzealous "when Errors.noncritical" | letouzey | 2013-03-17 |
* | Retyping.get_type_of: a lax version raising no anomalies | letouzey | 2013-03-17 |
* | Restrict (try...with...) to avoid catching critical exn (part 12) | letouzey | 2013-03-13 |
* | Added propagation of evars unification failure reasons for better | herbelin | 2013-02-17 |
* | Actually adding backtrace handling. | ppedrot | 2013-01-28 |
* | Uniformization of the "anomaly" command. | ppedrot | 2013-01-28 |
* | Added backtrace information to anomalies | ppedrot | 2013-01-28 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Modulification of identifier | ppedrot | 2012-12-14 |
* | Monomorphization (pretyping) | ppedrot | 2012-11-22 |
* | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey | 2012-10-02 |
* | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot | 2012-09-14 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | This patch removes unused "open" (automatically generated from | regisgia | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Practical fix for bug #1206 (anomaly raised in pretyping instead of | herbelin | 2012-07-06 |
* | Cleaning opening of the standard List module. | ppedrot | 2012-06-28 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Forward-port fixes from 8.4 (15358, 15353, 15333). | msozeau | 2012-06-04 |
* | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey | 2012-05-29 |
* | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey | 2012-05-29 |
* | Fix interface of resolve_typeclasses: onlyargs -> with_goals: | msozeau | 2012-03-20 |
* | More adaptations of pretyping/coercion to Program mode. | msozeau | 2012-03-19 |
* | Fix merge and add missing file. | msozeau | 2012-03-14 |
* | Revise API of understand_ltac to be parameterized by a flag for resolution of... | msozeau | 2012-03-14 |
* | Merge fixes | msozeau | 2012-03-14 |
* | Everything compiles again. | msozeau | 2012-03-14 |
* | Second step of integration of Program: | msozeau | 2012-03-14 |
* | Remove support for "abstract typing constraints" that requires unicity of sol... | msozeau | 2012-03-14 |
* | A bit of cleaning: unifying push_rels and push_rel_context. | herbelin | 2012-03-13 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Remove dynamic stuff from constr_expr and glob_constr | glondu | 2011-10-28 |
* | Now consider remaining conversion problems in solve_remaining_evars. | herbelin | 2011-10-22 |