diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.ml | 7 | ||||
| -rw-r--r-- | pretyping/evarsolve.ml | 2 | ||||
| -rw-r--r-- | pretyping/program.ml | 6 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 2 | ||||
| -rw-r--r-- | pretyping/unification.ml | 7 |
5 files changed, 13 insertions, 11 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b7fc2de95..51d006e25 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -45,12 +45,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 = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index a744f5ec6..c44903e8c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1591,6 +1591,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/program.ml b/pretyping/program.ml index b4333847b..4b6137b53 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 (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) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index e4cca2679..8ca40f829 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 diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5d6c41103..a96a496b8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1270,8 +1270,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] @@ -1390,7 +1389,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 |