From 0b417c12eb10bb29bcee04384b6c0855cb9de73a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 5 Oct 2016 17:50:45 +0200 Subject: unification.ml: fix for bug #4763, unif regression Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too. --- pretyping/evarsolve.ml | 2 ++ pretyping/unification.ml | 3 +-- 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 0db309f948..4084ee579a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1580,6 +1580,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) +(* This criterion relies on the fact that we postpone only problems of the form: +?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 347bf6f9e5..3d734ea9a9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1244,8 +1244,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] -- cgit v1.2.3 From 08f4cfc9dfb03973ae652ef6576342ae38f8f199 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 11:21:10 +0200 Subject: w_merge: Add a comment about the (List.rev evars) This change exposed bug #4763 --- pretyping/unification.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3d734ea9a9..b7edd6fcd6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1361,7 +1361,9 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd [] [] eqns in let res = (* merge constraints *) - w_merge_rec evd (order_metas metas) (List.rev evars) [] + w_merge_rec evd (order_metas metas) + (* Assign evars in the order of assignments during unification *) + (List.rev evars) [] in if with_types then check_types res else res -- cgit v1.2.3 From 0a6f0c161756a1878dd81e438df86f08631d8399 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 11:38:06 +0200 Subject: evarconv.ml: Fix bug #4529, primproj unfolding Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that. --- pretyping/evarconv.ml | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aead1cb35f..0d261f7f87 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -39,12 +39,7 @@ let _ = Goptions.declare_bool_option { let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - let c' = Some (mkProj (Projection.make cst true, c)) in - match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> c' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else c' + Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = -- cgit v1.2.3 From d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Oct 2016 18:06:47 +0200 Subject: Fix bug #4464: "Anomaly: variable H' unbound. Please report.". We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel. --- pretyping/retyping.mli | 2 ++ 1 file changed, 2 insertions(+) (limited to 'pretyping') diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index e4cca2679c..8ca40f829f 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr + +val print_retype_error : retype_error -> Pp.std_ppcmds -- cgit v1.2.3 From 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 8 Oct 2016 01:46:09 +0200 Subject: Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq. --- pretyping/program.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/program.ml b/pretyping/program.ml index b4333847b7..62aedcfbf6 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -15,10 +15,12 @@ open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) + user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) -- cgit v1.2.3