aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Expand)Author
2011-04-08Applying and reworking Tom Prince's patch for test-suite/failure/universes2.vherbelin
2011-04-08Replaced printing number of ill-typed branch by printing name of constructorherbelin
2011-04-06A few extra combinators about rel_declaration/named_declaration + a bit of docherbelin
2011-03-31As remarked by Enrico, we'd better use eq_constr than structural equalityherbelin
2011-03-23- Remove useless grammar rulemsozeau
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...msozeau
2011-03-13Fix inductive_template building ill-typed evars, and update test-suite scriptsmsozeau
2011-03-13- Add modulo_delta_types flag for unification to allow fullmsozeau
2011-03-11Keep information on which fields are subclasses in class declarations,msozeau
2011-03-11Tentative to make unification check types at every instanciation of anmsozeau
2011-03-11- Better error messages taking unif. constraints into account.msozeau
2011-03-10Forgot a use of evars_reset_evd in nf_evars, add an optional argument asmsozeau
2011-03-10Do not forget conv_pbs when resetting an evm: msozeau
2011-03-08Solve evar instantiations in the right environment.msozeau
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Revert commit r13883: instantiating ?n by a lambda when "?n a" has toherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2011-03-05Added a table for using reserved names for binding names to typesherbelin
2011-03-05A few more betaiota on environments and types of error messages. Seems toherbelin
2011-03-05Added support for instantiation of ?n by a lambda when "?n a" has toherbelin
2011-03-05Reorganized a bit evarconv.ml:herbelin
2011-03-05Improved define_evar_as_lambda which was creating an unrelated new evarherbelin
2011-03-05Instantiate evar by a lambda when "?n args" has to unify with Prodherbelin
2011-02-17- Use transparency information all the way through unification andmsozeau
2011-02-14- Fix treatment of globality flag for typeclass instance hints (theymsozeau
2011-02-11An automatic substitution of scope at functor applicationletouzey
2011-02-11In evars_of_term and co, visit array c in Evar(_,c) (sequel to r13809)letouzey
2011-02-03Repair Class_tactics.split_evars, broken by r13717 (should fix #2481)letouzey
2011-01-27Make simpl use the proper constant when folding (mutual) fixpointsletouzey
2011-01-11ratrapage exception, deja fait ...bgregoir
2011-01-07Fixing an uncaught exception bug with use of vmcastherbelin
2011-01-07mli comments for docpboutill
2010-12-25Rename mkR* smart constructors (mostly in funind)glondu
2010-12-24More {raw => glob} changes for consistencyglondu
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-12-19Fixing bug #2454: inversion predicate strategy for inferring the typeherbelin
2010-12-18Univ.constraints made fully abstract instead of being a Set of abstract stuffletouzey
2010-12-15Misc improvements about evar_mapletouzey
2010-11-08Refresh universes in params when generating schemes (Closes: #2429)glondu
2010-11-07Delayed the evar normalization in error messages to the last minuteherbelin
2010-10-31An experimental support for open constrs in hints and in "using"herbelin
2010-10-31Cleaning the use of parentheses around evd and evdref (cosmetic commit).herbelin
2010-10-31Slight cosmetic cleaning of tacred.ml.herbelin
2010-10-06Fixing the Not_found error in bug #2404 + dead code removal in cases.mlherbelin
2010-09-30Improve handling of metas as evars in unification (patch by Hugo)letouzey
2010-09-30Speed-up refine by avoiding some calls to Evd.foldletouzey
2010-09-28Fix bug #2321, allowing "_" named projections in classes. Not realizingmsozeau
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-28Remove "init" label from Termops.it_mk* specialized functionsglondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 14:58:44 +0000