From 64da3b4eac7d8d35bfd983e9f73bd1ff1bdcc216 Mon Sep 17 00:00:00 2001 From: msozeau Date: Wed, 22 Mar 2006 18:55:41 +0000 Subject: Subtac fixes, single fixpoint definitions are working again. Added a toggle on the pretyping module to allow or disallow binding of syntaxically inexistant variables (i.e., under an if when applied to an inductive where constructors have arguments). Does not change current behavior. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8655 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/subtac_command.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'contrib/subtac/subtac_command.ml') diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 64aee76119..5659950bc9 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -50,8 +50,9 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c'' = Subtac_interp_fixpoint.rewrite_cases c' in - Evd.evars_of !isevars, SPretyping.pretype_gen isevars env ([],[]) kind c'' + let c' = Subtac_interp_fixpoint.rewrite_cases env c' in + let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in + non_instanciated_map env isevars, c' let interp_constr isevars env c = interp_gen (OfType None) isevars env c -- cgit v1.2.3