Passage à des contextes de vars et de rels pouvant contenir des déclarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 87 insertions, 81 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 08c740013..60d9e5f13 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -91,8 +91,9 @@ let hypothesis_def_var is_refining ident n c =
 	parameter_def_var ident c
     | DischargeAt disch_sp ->
         if Lib.is_section_p disch_sp then begin
+	  let t = interp_type Evd.empty (Global.env()) c in
           declare_variable (id_of_string ident)
-             (interp_type Evd.empty (Global.env()) c,n,false);
+             (SectionLocalDecl t,n,false);
 	  if is_verbose() then message (ident ^ " is assumed");
           if is_refining then 
             mSGERRNL [< 'sTR"Warning: Variable "; 'sTR ident; 
@@ -145,7 +146,7 @@ let build_mutual lparams lnamearconstrs finite =
 	(fun (env,arl) (recname,arityc,_) -> 
            let arity =
 	     typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
-	   let env' = Environ.push_rel (Name recname,arity) env in
+	   let env' = Environ.push_rel_decl (Name recname,arity) env in
 	   (env', (arity::arl)))
 	(env0,[]) lnamearconstrs 
     in
@@ -218,8 +219,8 @@ let build_recursive lnameargsardef =
       List.fold_left 
         (fun (env,arl) (recname,lparams,arityc,_) -> 
            let arity = typed_type_of_com Evd.empty env (mkProdCit lparams arityc) in
-           declare_variable recname (body_of_type arity,NeverDischarge,false);
-           (Environ.push_var (recname,arity) env, (arity::arl)))
+           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
       States.unfreeze fs; raise e
@@ -281,8 +282,8 @@ let build_corecursive lnameardef =
       List.fold_left 
         (fun (env,arl) (recname,arityc,_) -> 
            let arity = typed_type_of_com Evd.empty env0 arityc in
-           declare_variable recname (body_of_type arity,NeverDischarge,false);
-           (Environ.push_var (recname,arity) env, (arity::arl)))
+           declare_variable recname (SectionLocalDecl (body_of_type arity),NeverDischarge,false);
+           (Environ.push_var_decl (recname,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
       States.unfreeze fs; raise e
@@ -376,15 +377,17 @@ let start_proof_com sopt stre com =
   Pfedit.start_proof id stre env (interp_type Evd.empty env com)
 
 let save_named opacity =
-  let id,(const,strength) = Pfedit.release_proof () in
+  let id,(const,strength) = Pfedit.cook_proof () in
   declare_constant id (const,strength);
+  Pfedit.delete_current_proof ();
   if Options.is_verbose() then message ((string_of_id id) ^ " is defined")
 
 let save_anonymous opacity save_ident strength =
-  let id,(const,_) = Pfedit.release_proof () in
+  let id,(const,_) = Pfedit.cook_proof () in
   if atompart_of_id id <> "Unnamed_thm" then
     message("Overriding name "^(string_of_id id)^" and using "^save_ident);
   declare_constant (id_of_string save_ident) (const,strength);
+  Pfedit.delete_current_proof ();
   if Options.is_verbose() then message (save_ident ^ " is defined")
 
 let save_anonymous_thm opacity id =
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index ebf70569d..91ce37753 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -26,8 +26,7 @@ let recalc_sp sp =
 
 let whd_all c = whd_betadeltaiota (Global.env()) Evd.empty c
 
-let generalize_type id var c =
-  typed_product_without_universes (Name id) var (typed_app (subst_var id) c)
+let generalize_type = generalize_without_universes
 
 type modification_action = ABSTRACT | ERASE
 
@@ -100,16 +99,16 @@ let under_dlams f =
   apprec 
 
 let abstract_inductive ids_to_abs hyps inds =
-  let abstract_one_var id ty inds =
+  let abstract_one_var d inds =
     let ntyp = List.length inds in 
     let new_refs = list_tabulate (fun k -> applist(Rel (k+2),[Rel 1])) ntyp in 
     let inds' =
       List.map
       	(function (tname,arity,cnames,lc) -> 
-	   let arity' = generalize_type id ty arity in
+	   let arity' = generalize_type d arity in
 	   let lc' =
 	     List.map
-	       (fun b -> generalize_type id ty (typed_app (substl new_refs) b))
+	       (fun b -> generalize_type d (typed_app (substl new_refs) b))
 	       lc
 	   in
            (tname,arity',cnames,lc'))
@@ -118,11 +117,13 @@ let abstract_inductive ids_to_abs hyps inds =
     (inds',ABSTRACT)
   in
   let abstract_once ((hyps,inds,modl) as sofar) id =
-    if isnull_sign hyps or id <> fst (hd_sign hyps) then 
-      sofar
-    else
-      let (inds',modif) = abstract_one_var id (snd (hd_sign hyps)) inds in 
-      (tl_sign hyps,inds',modif::modl)
+    match hyps with
+      | [] -> sofar
+      | (hyp,c,t as d)::rest ->
+	  if id <> hyp then sofar
+	  else
+	    let (inds',modif) = abstract_one_var d inds in 
+	    (rest, inds', modif::modl)
   in
   let (_,inds',revmodl) =
     List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
@@ -134,22 +135,20 @@ let abstract_inductive ids_to_abs hyps inds =
 
 let abstract_constant ids_to_abs hyps (body,typ) =
   let abstract_once ((hyps,body,typ,modl) as sofar) id =
-    if isnull_sign hyps or id <> fst(hd_sign hyps) then 
-      sofar
+    match hyps with
+      | [] -> sofar
+      | (hyp,c,t as decl)::rest ->
+    if hyp <> id then sofar
     else
-      let name = Name id in
-      let var = snd (hd_sign hyps) in
-      let cvar = incast_type var in
       let body' = match body with
 	| None -> None
 	| Some { contents = Cooked c } -> 
-	    Some (ref (Cooked (mkLambda name cvar (subst_var id c))))
+	    Some (ref (Cooked (mkNamedLambda_or_LetIn decl c)))
 	| Some { contents = Recipe f } ->
-	    Some (ref (Recipe 
-			 (fun () -> mkLambda name cvar (subst_var id (f())))))
+	    Some (ref (Recipe (fun () -> mkNamedLambda_or_LetIn decl (f()))))
       in
-      let typ' = generalize_type id var typ in
-      (tl_sign hyps,body',typ',ABSTRACT::modl)
+      let typ' = generalize_type decl typ in
+      (rest, body', typ', ABSTRACT::modl)
   in
   let (_,body',typ',revmodl) =
     List.fold_left abstract_once (hyps,body,typ,[]) ids_to_abs in
@@ -244,7 +243,7 @@ let process_constant osecsp nsecsp oldenv (ids_to_discard,modlist) cb =
   let body = 
     expmod_constant_value cb.const_opaque oldenv modlist cb.const_body in
   let typ = expmod_type oldenv modlist cb.const_type in
-  let hyps = map_sign_typ (expmod_type oldenv modlist) cb.const_hyps in
+  let hyps = map_var_context (expmod_constr oldenv modlist) cb.const_hyps in
   let (body',typ',modl) = abstract_constant ids_to_discard hyps (body,typ) in
   let mods = [ (Const osecsp, DO_ABSTRACT(Const nsecsp,modl)) ] in
   (body', body_of_type typ', mods)
@@ -267,7 +266,7 @@ let inductive_message inds =
 			 'sPC; 'sTR "are discharged.">]))
 
 type discharge_operation = 
-  | Variable of identifier * constr * strength * bool
+  | Variable of identifier * section_variable_entry * strength * bool
   | Parameter of identifier * constr
   | Constant of identifier * constant_entry * strength
   | Inductive of mutual_inductive_entry
@@ -280,13 +279,20 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
   let tag = object_tag lobj in 
   match tag with
     | "VARIABLE" ->
-	let (id,a,stre,sticky) = out_variable sp in
+	let ((id,c,t),stre,sticky) = out_variable sp in
 	if stre = (DischargeAt sec_sp) or ids_to_discard <> [] then
 	  (ops,id::ids_to_discard,work_alist)
 	else
-	  let expmod_a = expmod_constr oldenv work_alist (body_of_type a) in
-	  (Variable (id,expmod_a,stre,sticky) :: ops,
-           ids_to_discard,work_alist)
+	  let newdecl =
+	    match c with
+	      | None ->
+		  SectionLocalDecl
+		    (expmod_constr oldenv work_alist (body_of_type t))
+	      | Some body ->
+		  SectionLocalDef
+		    (expmod_constr oldenv work_alist body)
+	  in
+	  (Variable (id,newdecl,stre,sticky) :: ops, ids_to_discard,work_alist)
 
     | "CONSTANT" | "PARAMETER" ->
 	let stre = constant_or_parameter_strength sp in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 413aafce6..9608f5af5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -22,15 +22,16 @@ let guill s = "\""^s^"\""
 
 let explain_unbound_rel k ctx n =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in
   [< 'sTR"Unbound reference: "; pe; 'fNL;
      'sTR"The reference "; 'iNT n; 'sTR" is free" >]
 
 let explain_not_type k ctx j =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR"In environment" >] k ctx in
   let pc,pt = prjudge_env ctx j in
-  [< pe; 'cUT; 'sTR "the term"; 'bRK(1,1); pc; 'sPC; 'sTR"has type"; 'sPC; 
+  [< pe; 'fNL; 'sTR "the term"; 'bRK(1,1); pc; 'sPC;
+     'sTR"has type"; 'sPC; pt; 'sPC; 
      'sTR"which should be Set, Prop or Type." >];;
 
 let explain_bad_assumption k ctx c =
@@ -92,9 +93,9 @@ let explain_ill_formed_branch k ctx c i actty expty =
 
 let explain_generalization k ctx (name,var) j =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in
   let pv = prtype_env ctx var in
-  let (pc,pt) = prjudge_env (add_rel (name,var) ctx) j in
+  let (pc,pt) = prjudge_env (push_rel_decl (name,var) ctx) j in
   [< 'sTR"Illegal generalization: "; pe; 'fNL;
      'sTR"Cannot generalize"; 'bRK(1,1); pv; 'sPC;
      'sTR"over"; 'bRK(1,1); pc; 'sTR","; 'sPC; 'sTR"it has type"; 'sPC; pt; 
@@ -102,7 +103,7 @@ let explain_generalization k ctx (name,var) j =
 
 let explain_actual_type k ctx c ct pt =
   let ctx = make_all_name_different ctx in
-  let pe = pr_ne_env [< 'sTR"In environment" >] k ctx in
+  let pe = pr_ne_context_of [< 'sTR"In environment" >] k ctx in
   let pc = prterm_env ctx c in
   let pct = prterm_env ctx ct in
   let pt = prterm_env ctx pt in
@@ -113,10 +114,14 @@ let explain_actual_type k ctx c ct pt =
 
 let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
   let ctx = make_all_name_different ctx in
-(*  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in*)
+(*  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in*)
   let pr,prt = prjudge_env ctx rator in
-  let term_string = if List.length randl > 1 then "terms" else "term" in
-  let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
+  let term_string1,term_string2 =
+    if List.length randl > 1 then
+      let many = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
+      "terms", "The "^(string_of_int n)^many^" term"
+    else
+      "term","This term" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
 		  let pc,pct = prjudge_env ctx c in
@@ -125,15 +130,14 @@ let explain_cant_apply_bad_type k ctx (n,exptyp,actualtyp) rator randl =
   [< 'sTR"Illegal application (Type Error): "; (* pe; *) 'fNL;
      'sTR"The term"; 'bRK(1,1); pr; 'sPC;
      'sTR"of type"; 'bRK(1,1); prt; 'sPC ;
-     'sTR("cannot be applied to the "^term_string); 'fNL; 
+     'sTR("cannot be applied to the "^term_string1); 'fNL; 
      'sTR" "; v 0 appl; 'fNL;
-     'sTR"The ";'iNT n; 'sTR (many^" term of type"); 'bRK(1,1); 
-     prterm_env ctx actualtyp; 'sPC;
-     'sTR"should be coercible to"; 'bRK(1,1); prterm_env ctx exptyp >]
+     'sTR (term_string2^" has type"); 'bRK(1,1); prterm_env ctx exptyp; 'sPC;
+     'sTR"which should be coercible to"; 'bRK(1,1); prterm_env ctx actualtyp >]
 
 let explain_cant_apply_not_functional k ctx rator randl =
   let ctx = make_all_name_different ctx in
-(*  let pe = pr_ne_env [< 'sTR"in environment" >] k ctx in*)
+(*  let pe = pr_ne_context_of [< 'sTR"in environment" >] k ctx in*)
   let pr = prterm_env ctx rator.uj_val in
   let prt = prterm_env ctx (body_of_type rator.uj_type) in
   let term_string = if List.length randl > 1 then "terms" else "term" in
@@ -356,22 +360,19 @@ let explain_refiner_error = function
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | BadTacticArgs (s,l) -> explain_refiner_bad_tactic_args s l
 
-let error_non_strictly_positive k lna c v  =
-  let env = assumptions_for_print lna in
+let error_non_strictly_positive k env c v  =
   let pc = prterm_env env c in
   let pv = prterm_env env v in
   [< 'sTR "Non strictly positive occurrence of "; pv; 'sTR " in";
      'bRK(1,1); pc >]
 
-let error_ill_formed_inductive k lna c v =
-  let env = assumptions_for_print lna in
+let error_ill_formed_inductive k env c v =
   let pc = prterm_env env c in
   let pv = prterm_env env v in
   [< 'sTR "Not enough arguments applied to the "; pv;
      'sTR " in"; 'bRK(1,1); pc >]
 
-let error_ill_formed_constructor k lna c v =
-  let env = assumptions_for_print lna in
+let error_ill_formed_constructor k env c v =
   let pc = prterm_env env c in
   let pv = prterm_env env v in
   [< 'sTR "The conclusion of"; 'bRK(1,1); pc; 'bRK(1,1); 
@@ -385,8 +386,7 @@ let str_of_nth n =
      | 3 -> "rd"
      | _ -> "th")
 
-let error_bad_ind_parameters k lna c n v1 v2  =
-  let env = assumptions_for_print lna in
+let error_bad_ind_parameters k env c n v1 v2  =
   let pc = prterm_env_at_top env c in
   let pv1 = prterm_env env v1 in
   let pv2 = prterm_env env v2 in
@@ -412,7 +412,7 @@ let error_not_allowed_case_analysis dep kind i =
   [< 'sTR (if dep then "Dependent" else "Non Dependent");
      'sTR " case analysis on sort: "; print_sort kind; 'fNL;
      'sTR "is not allowed for inductive definition: ";
-     pr_inductive (Global.context()) i >]
+     pr_inductive (Global.env()) i >]
 
 let error_bad_induction dep indid kind =
   [<'sTR (if dep then "Dependent" else "Non dependend");
@@ -425,10 +425,10 @@ let error_not_mutual_in_scheme () =
 
 let explain_inductive_error = function
   (* These are errors related to inductive constructions *)
-  | NonPos (lna,c,v) -> error_non_strictly_positive CCI lna c v
-  | NotEnoughArgs (lna,c,v) -> error_ill_formed_inductive CCI lna c v
-  | NotConstructor (lna,c,v) -> error_ill_formed_constructor CCI lna c v
-  | NonPar (lna,c,n,v1,v2) -> error_bad_ind_parameters CCI lna c n v1 v2
+  | NonPos (env,c,v) -> error_non_strictly_positive CCI env c v
+  | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive CCI env c v
+  | NotConstructor (env,c,v) -> error_ill_formed_constructor CCI env c v
+  | NonPar (env,c,n,v1,v2) -> error_bad_ind_parameters CCI env c n v1 v2
   | SameNamesTypes id -> error_same_names_types id
   | SameNamesConstructors (id,cid) -> error_same_names_constructors id cid
   | NotAnArity id -> error_not_an_arity id
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index edebaaf52..fabe32634 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -5,14 +5,14 @@
 open Pp
 open Names
 open Indtypes
-open Sign
+open Environ
 open Type_errors
 open Logic
 (*i*)
 
 (* This module provides functions to explain the type errors. *)
 
-val explain_type_error : path_kind -> context -> type_error -> std_ppcmds
+val explain_type_error : path_kind -> env -> type_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 268ebd437..0fc6f85a8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -72,14 +72,14 @@ let typecheck_params_and_field ps fs =
     List.fold_left
       (fun (env,newps) (id,t) -> 
          let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var (id,tj) env,(id,body_of_type tj)::newps))
+         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newps))
       (env0,[]) ps
   in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) (id,t) -> 
          let tj = typed_type_of_com Evd.empty env t in
-         (Environ.push_var (id,tj) env,(id,body_of_type tj)::newfs)) (env1,[]) fs
+         (Environ.push_var_decl (id,tj) env,(id,body_of_type tj)::newfs)) (env1,[]) fs
   in
   List.rev(newps),List.rev(newfs)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d483b1e6a..32a30d144 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -48,13 +48,13 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSGNL(Refiner.print_script true (ts_it evc) (Global.var_context()) pf)
+  mSGNL(Refiner.print_script true evc (Global.var_context()) pf)
 
 let show_prooftree () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  mSG(Refiner.print_proof (ts_it evc) (Global.var_context()) pf)
+  mSG(Refiner.print_proof evc (Global.var_context()) pf)
 
 let show_open_subgoals () =
   let pfts = get_pftreestate () in
@@ -83,7 +83,6 @@ let show_open_subgoals_focused () =
 let show_node () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
-  and evc = evc_of_pftreestate pts
   and cursor = cursor_of_pftreestate pts in
   mSG [< prlist_with_sep pr_spc pr_int (List.rev cursor); 'fNL ;
          prgl pf.goal ; 'fNL ;
@@ -214,7 +213,7 @@ let _ =
 (* Managing states *)
 
 let abort_refine f x =
-  if Pfedit.refining() then abort_all_proofs ();
+  if Pfedit.refining() then delete_all_proofs ();
   f x
   (* used to be: error "Must save or abort current goal first" *)
 
@@ -352,10 +351,10 @@ let _ =
     (function 
        | [VARG_IDENTIFIER id] -> 
 	   (fun () -> 
-	      abort_proof id;
+	      delete_proof id;
 	      message ("Goal "^(string_of_id id)^" aborted"))
        | [] -> (fun () -> 
-		  abort_current_proof ();
+		  delete_current_proof ();
 		  message "Current goal aborted")
        | _  -> bad_vernac_args "ABORT")
 
@@ -364,7 +363,7 @@ let _ =
     (function 
        | [] -> (fun () ->
 		  if refining() then begin
-		    abort_all_proofs ();
+		    delete_all_proofs ();
 		    message "Current goals aborted"
 		  end else
 		    error "No proof-editing in progress")
@@ -529,15 +528,14 @@ let _ =
 	      let pts = get_pftreestate () in
 	      let pf = proof_of_pftreestate pts in
 	      let cursor = cursor_of_pftreestate pts in
-	      let evc = ts_it (evc_of_pftreestate pts) in
-	      let (pfterm,meta_types) = 
-		Refiner.extract_open_proof (var_context pf.goal.evar_env) pf in
+	      let evc = evc_of_pftreestate pts in
+	      let (pfterm,meta_types) = extract_open_pftreestate pts in
 	      mSGNL [< 'sTR"LOC: " ;
 		       prlist_with_sep pr_spc pr_int (List.rev cursor); 'fNL ;
 		       'sTR"Subgoals" ; 'fNL ;
 		       prlist
 			 (fun (mv,ty) -> 
-			    [< 'iNT mv ; 'sTR" -> " ; prterm ty ; 'fNL >])
+			    [< 'iNT mv ; 'sTR" -> " ; prtype ty ; 'fNL >])
 			 meta_types;
 		       'sTR"Proof: " ; prterm (nf_ise1 evc pfterm) >])
        | _ -> bad_vernac_args "ShowProof")
@@ -550,8 +548,7 @@ let _ =
 	      let pts = get_pftreestate () in
 	      let pf = proof_of_pftreestate pts 
 	      and cursor = cursor_of_pftreestate pts in
-	      let (pfterm,meta_types) = 
-		Refiner.extract_open_proof (var_context pf.goal.evar_env) pf in
+	      let (pfterm,_) = extract_open_pftreestate pts in
 	      let message = 
 		try 
 		  Typeops.control_only_guard pf.goal.evar_env 
@@ -590,7 +587,7 @@ let _ =
            | (n::l) -> aux (Tacmach.traverse n pts) l in 
          let pts = aux pts (l@[-1]) in
          let pf = proof_of_pftreestate pts in 
-	 mSG (Refiner.print_script true (ts_it evc) (Global.var_context()) pf))
+	 mSG (Refiner.print_script true evc (Global.var_context()) pf))
 
 let _ =
   add "ExplainProofTree"
@@ -607,7 +604,7 @@ let _ =
            | (n::l) -> aux (Tacmach.traverse n pts) l in 
          let pts = aux pts (l@[-1]) in
          let pf = proof_of_pftreestate pts in 
-	 mSG (Refiner.print_proof (ts_it evc) (Global.var_context()) pf))
+	 mSG (Refiner.print_proof evc (Global.var_context()) pf))
 
 let _ =
   add "ShowProofs"
@@ -719,7 +716,7 @@ let _ =
                   mSGNL [< 'sTR"Error: checking of theorem " ; print_id s ;
                            'sPC ; 'sTR"failed" ;
                            'sTR"... converting to Axiom" >];
-                  abort_proof s;
+                  delete_proof s;
                   parameter_def_var (string_of_id s) com
            	end else 
 		  errorlabstrm "vernacentries__TheoremProof"