diff options
Diffstat (limited to 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 42 |
1 files changed, 25 insertions, 17 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 29cad063..0d197c92 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -13,35 +15,41 @@ open Evd open Evarutil open Evarsolve open Pp +open Glob_term +open Ltac_pretype (******************************************) (* Instantiation of existential variables *) (******************************************) -let depends_on_evar evk _ (pbty,_,t1,t2) = - try Evar.equal (head_evar t1) evk +type glob_constr_ltac_closure = ltac_var_map * glob_constr + +let depends_on_evar sigma evk _ (pbty,_,t1,t2) = + let t1 = EConstr.of_constr t1 in + let t2 = EConstr.of_constr t2 in + try Evar.equal (head_evar sigma t1) evk with NoHeadEvar -> - try Evar.equal (head_evar t2) evk + try Evar.equal (head_evar sigma t2) evk with NoHeadEvar -> false let define_and_solve_constraints evk c env evd = - if Termops.occur_evar evk c then + if Termops.occur_evar evd evk c then Pretype_errors.error_occur_check env evd evk c; - let evd = define evk c evd in - let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in + let evd = define evk (EConstr.Unsafe.to_constr c) evd in + let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in match List.fold_left (fun p (pbty,env,t1,t2) -> match p with - | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2) | UnifFailure _ as x -> x) (Success evd) pbs with | Success evd -> evd - | UnifFailure _ -> error "Instance does not satisfy the constraints." + | UnifFailure _ -> user_err Pp.(str "Instance does not satisfy the constraints.") let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then - error "Instantiate called on already-defined evar"; + user_err Pp.(str "Instantiate called on already-defined evar"); let env = Evd.evar_filtered_env evi in let sigma',typed_c = let flags = { @@ -51,11 +59,11 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = Pretyping.fail_evar = false; Pretyping.expand_evars = true } in try Pretyping.understand_ltac flags - env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc + env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc with e when CErrors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in - user_err_loc - (loc,"", str "Instance is not well-typed in the environment of " ++ - pr_existential_key sigma evk ++ str ".") + user_err ?loc + (str "Instance is not well-typed in the environment of " ++ + Termops.pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) |