From e875e90d1d90aec22e6f206f04c4941cb5a3bcd1 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 30 Nov 2013 19:34:46 +0100 Subject: Fixing ltac constr variable handling in refine. --- proofs/goal.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'proofs/goal.mli') diff --git a/proofs/goal.mli b/proofs/goal.mli index 1f04ce8c1..013b3199a 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -93,8 +93,8 @@ module Refinable : sig The principal argument is a [glob_constr] which is then pretyped in the context of a term, the remaining evars are registered to the handle. It is the main component of the toplevel refine tactic.*) - val constr_of_raw : - handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive + val constr_of_raw : handle -> bool -> bool -> Pretyping.ltac_var_map -> + Glob_term.glob_constr -> Term.constr sensitive (* [constr_of_open_constr h check_type] transforms an open constr into a goal-sensitive constr, adding the undefined variables to the set of subgoals. -- cgit v1.2.3