aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
AgeCommit message (Expand)Author
2011-10-25Continuing r14585 (ill-typed restriction bug).herbelin
2011-10-25Continuing r1492 (useless changes were inadvertantly committed)herbelin
2011-10-25New strategy to infer return predicate of match construct whenherbelin
2011-10-24Fixing another bug revealing ill-typed use of evar restriction.herbelin
2011-10-24Fixing instance/filter mismatch in materialize_evar + documentation.herbelin
2011-10-17Partly reverting r14539 about fully expanding "let-in"s and not justherbelin
2011-10-10More robust and uniform treatment of aliases in evarutil.mlherbelin
2011-10-10Applied the trick of Chung-Kil Hur to solve second-order matchingherbelin
2011-10-10Fixing buggy abberant code for Evarutil.expand_evarherbelin
2011-10-10Passed conv_algo to evar_define and move call to solve_refl toherbelin
2011-08-03Fix nf_evars_undefinedmsozeau
2011-07-29Evarutil: replace generic list_distinct on constr by constr_list_distinctpuech
2011-07-29Evarutil: replaced some generic = on constr by destructorspuech
2011-07-29Evarutil: generic equality on constr replaced by destructorspuech
2011-07-29Evarutil: generic equality on constr replaced by eq_constr (x2)puech
2011-07-29Evarutil: generic equality on constr replaced by eq_constrpuech
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing constrai...msozeau
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
2011-06-08Fixes in pruning in unification.msozeau
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to typechec...msozeau
2011-04-13- Make typeclass transparency information directly availablemsozeau
2011-04-13- Remove create_evar_defsmsozeau
2011-04-11Catch NotArity exception and transform it into an anomaly in retyping.msozeau
2011-03-23- Fix solve_simpl_eqn which was cheking instances types in the wrong environm...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-07Reverted commit r13893 about propagation of more informativeherbelin
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-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-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
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-09-30Speed-up refine by avoiding some calls to Evd.foldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-30Fix (part of) bug #2347, de Bruijn bug in Program's pretyper.msozeau
2010-06-29Made tclABSTRACT normalize evars before saying it does not supportherbelin
2010-06-12Added rudimentary support for using constructors from the explicitherbelin
2010-06-12Fixed a bug in evarutil.ml (wrong env of a postponed conversion problem).herbelin
2010-06-11Mainly made that evarconv is able to solve "?n = (fun x => x) ?n" (sic).herbelin
2010-05-26Fixing Derive Inversion for new proof engineherbelin
2010-05-13Improved the efficiency of evars traverals thanks to a split ofherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2010-04-20Fixed bugs from commit 12954 on unification complexityherbelin
2010-04-19Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).herbelin
2009-12-21Generic support for open terms in tacticsherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-28 06:59:48 +0000