aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
Commit message (Expand)AuthorAge
* TC: honor the use_typeclasses flag in pretypingGravatar Enrico Tassi2014-02-12
* Support for evars and metas in native compiler.Gravatar Maxime Dénès2013-12-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Using the whole tactic environment while Pretyping.Gravatar ppedrot2013-06-24
* Generalizing the use of maps instead of lists in the interpretationGravatar ppedrot2013-06-22
* A uniformization step around understand_* and interp_* functions.Gravatar herbelin2013-05-09
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Avoid a few overzealous "when Errors.noncritical"Gravatar letouzey2013-03-17
* Retyping.get_type_of: a lax version raising no anomaliesGravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 12)Gravatar letouzey2013-03-13
* Added propagation of evars unification failure reasons for betterGravatar herbelin2013-02-17
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Added backtrace information to anomaliesGravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (pretyping)Gravatar ppedrot2012-11-22
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Practical fix for bug #1206 (anomaly raised in pretyping instead ofGravatar herbelin2012-07-06
* Cleaning opening of the standard List module.Gravatar ppedrot2012-06-28
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Forward-port fixes from 8.4 (15358, 15353, 15333).Gravatar msozeau2012-06-04
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Glob_term now mli-only, operations now in Glob_opsGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Evar_kinds.mli containing former Evd.hole_kind, avoid deps on EvdGravatar letouzey2012-05-29
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* More adaptations of pretyping/coercion to Program mode.Gravatar msozeau2012-03-19
* Fix merge and add missing file.Gravatar msozeau2012-03-14
* Revise API of understand_ltac to be parameterized by a flag for resolution of...Gravatar msozeau2012-03-14
* Merge fixesGravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Second step of integration of Program:Gravatar msozeau2012-03-14
* Remove support for "abstract typing constraints" that requires unicity of sol...Gravatar msozeau2012-03-14
* A bit of cleaning: unifying push_rels and push_rel_context.Gravatar herbelin2012-03-13
* Noise for nothingGravatar pboutill2012-03-02
* Remove dynamic stuff from constr_expr and glob_constrGravatar glondu2011-10-28
* Now consider remaining conversion problems in solve_remaining_evars.Gravatar herbelin2011-10-22
* It happens that the type inference algorithm (pretyping) did not checkGravatar herbelin2011-10-05
* Moving implicit tactic support from Tacinterp to Pfedit and final evarGravatar herbelin2011-09-26
* Failing instead of switching to the coercion mechanism when VMcastGravatar herbelin2011-05-15
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13