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

10 files changed, 174 insertions, 169 deletions

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 66a2b3601..ced1756f1 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -24,27 +24,43 @@ let list_index x l =
 
 let list_assoc_index x l =
   let rec aux i = function
-      (k, v) :: tl -> if k = x then i else aux (succ i) tl
+      (k, _, v) :: tl -> if k = x then i else aux (succ i) tl
     | [] -> raise Not_found
   in aux 0 l
 
 (** Substitute evar references in t using De Bruijn indices, 
   where n binders were passed through. *)
 let subst_evars evs n t = 
-  let evar_index id = 
-    let idx = list_assoc_index id evs in
-      idx + 1
+  let evar_info id = 
+    let rec aux i = function
+	(k, h, v) :: tl -> if k = id then (i, h, v) else aux (succ i) tl
+      | [] -> raise Not_found
+    in 
+    let (idx, hyps, v) = aux 0 evs in
+      idx + 1, hyps
   in
   let rec substrec depth c = match kind_of_term c with
     | Evar (k, args) ->
 	(try 
-	   msgnl (str "Evar " ++ int k ++ str " found");
-	   let ex = 
-(* 	     mkVar (id_of_string ("Evar" ^ string_of_int k));*)
-  	     mkRel (evar_index k + depth)  
+	   let index, hyps = evar_info k in
+	     msgnl (str "Evar " ++ int k ++ str " found, applied to " ++ int (Array.length args) ++ str "arguments," ++
+		      int (List.length hyps) ++ str " hypotheses");
+
+	   let ex = mkRel (index + depth) in
+	     (* Evar arguments are created in inverse order, 
+		and we must not apply to defined ones (i.e. LetIn's)
+	     *)
+	   let args =
+	     let rec aux hyps args acc =
+	       match hyps, args with
+		   ((_, None, _) :: tlh), (c :: tla) -> 
+		     aux tlh tla ((map_constr_with_binders succ substrec depth c) :: acc)
+		 | ((_, Some _, _) :: tlh), (_ :: tla) ->
+		     aux tlh tla acc
+		 | [], [] -> acc
+		 | _, _ -> failwith "subst_evars: invalid argument"
+	     in aux hyps (Array.to_list args) [] 
 	   in
-	     (* Evar arguments are created in inverse order *)
-	   let args = List.rev_map (map_constr_with_binders succ substrec depth) (Array.to_list args) in
 	     mkApp (ex, Array.of_list args)
 	 with Not_found -> 
 	   msgnl (str "Evar " ++ int k ++ str " not found!!!");
@@ -70,7 +86,7 @@ let subst_vars acc n t =
   to a product : forall H1 : t1, ..., forall Hn : tn, concl.
   Changes evars and hypothesis references to De Bruijn indices.
 *)
-let etype_of_evar evs ev =
+let etype_of_evar evs ev hyps =
   let rec aux acc n = function
       (id, copt, t) :: tl ->
 	let t' = subst_evars evs n t in
@@ -79,7 +95,7 @@ let etype_of_evar evs ev =
     | [] ->
 	let t' = subst_evars evs n ev.evar_concl in
 	  subst_vars acc 0 t'	
-  in aux [] 0 (rev (Environ.named_context_of_val ev.evar_hyps))
+  in aux [] 0 (rev hyps)
 
 
 open Tacticals
@@ -91,8 +107,9 @@ let eterm evm t =
   let evts = 
     (* Remove existential variables in types and build the corresponding products *)
     fold_left 
-      (fun l (id, y) -> 
-	 let y' = (id, etype_of_evar l y) in
+      (fun l (id, ev) ->
+	 let hyps = Environ.named_context_of_val ev.evar_hyps in
+	 let y' = (id, hyps, etype_of_evar l ev hyps) in
 	   y' :: l) 
       [] evl 
   in 
@@ -102,7 +119,7 @@ let eterm evm t =
   let t'' = 
     (* Make the lambdas 'generalizing' the existential variables *)
     fold_left
-      (fun acc (id, c) ->
+      (fun acc (id, _, c) ->
 	 mkLambda (Name (id_of_string ("Evar" ^ string_of_int id)),
 		   c, acc))
       t' evts
@@ -116,7 +133,9 @@ let eterm evm t =
     let id = id_of_string ("Evar" ^ string_of_int id) in
       tclTHEN acc (Tactics.assert_tac false (Name id) c)
   in
-    msgnl (str "Term constructed in Eterm" ++
+    msgnl (str "Term given to eterm" ++ spc () ++
+	   Termops.print_constr_env (Global.env ()) t);
+    msgnl (str "Term constructed in eterm" ++ spc () ++
 	   Termops.print_constr_env (Global.env ()) t'');
     Tactics.apply_term t'' (List.map (fun _ -> Evarutil.mk_new_meta ()) evts)
      
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index 12755960e..01c959a47 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -114,6 +114,7 @@ let subtac_end_proof = function
     | Some ((_,id),Some kind) -> save_anonymous_with_strength kind is_opaque id
 
 	*)
+
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
@@ -139,7 +140,7 @@ let subtac (loc, command) =
 		     Pfedit.by tac)
       | VernacFixpoint (l, b) -> 
 	  let _ = trace (str "Building fixpoint") in
-	  ignore(Subtac_command.build_recursive l b)
+	    ignore(Subtac_command.build_recursive l b)
       (*| VernacEndProof e -> 
 	  subtac_end_proof e*)
 
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 64aee7611..5659950bc 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 
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 23a03290c..6c1b0103f 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -1,103 +1,42 @@
-module SPretyping :
-  sig
-    module Cases :
-      sig
-        val compile_cases :
-          Util.loc ->
-          (Evarutil.type_constraint ->
-           Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment) *
-          Evd.evar_defs ref ->
-          Evarutil.type_constraint ->
-          Environ.env ->
-          Rawterm.rawconstr option *
-          (Rawterm.rawconstr *
-           (Names.name *
-            (Util.loc * Names.inductive * Names.name list) option))
-          list *
-          (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
-           Rawterm.rawconstr)
-          list -> Environ.unsafe_judgment
-      end
-    val understand_tcc :
-      Evd.evar_map ->
-      Environ.env ->
-      ?expected_type:Term.types -> Rawterm.rawconstr -> Evd.open_constr
-    val understand_ltac :
-      Evd.evar_map ->
-      Environ.env ->
-      Pretyping.var_map * Pretyping.unbound_ltac_var_map ->
-      Pretyping.typing_constraint ->
-      Rawterm.rawconstr -> Evd.evar_defs * Term.constr
-    val understand :
-      Evd.evar_map ->
-      Environ.env ->
-      ?expected_type:Term.types -> Rawterm.rawconstr -> Term.constr
-    val understand_type :
-      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
-    val understand_gen :
-      Pretyping.typing_constraint ->
-      Evd.evar_map -> Environ.env -> Rawterm.rawconstr -> Term.constr
-    val understand_judgment :
-      Evd.evar_map ->
-      Environ.env -> Rawterm.rawconstr -> Environ.unsafe_judgment
-    val understand_judgment_tcc :
-      Evd.evar_map ->
-      Environ.env ->
-      Rawterm.rawconstr -> Evd.evar_map * Environ.unsafe_judgment
-    val pretype :
-      Evarutil.type_constraint ->
-      Environ.env ->
-      Evd.evar_defs ref ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Rawterm.rawconstr -> Environ.unsafe_judgment
-    val pretype_type :
-      Evarutil.val_constraint ->
-      Environ.env ->
-      Evd.evar_defs ref ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Rawterm.rawconstr -> Environ.unsafe_type_judgment
-    val pretype_gen :
-      Evd.evar_defs ref ->
-      Environ.env ->
-      Pretyping.var_map * (Names.identifier * Names.identifier option) list ->
-      Pretyping.typing_constraint -> Rawterm.rawconstr -> Term.constr
-  end
+open Pretyping
+open Evd
+open Environ
+open Term
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+
 val interp_gen :
-  Pretyping.typing_constraint ->
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
+  typing_constraint ->
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
   ?allow_soapp:bool ->
-  ?ltacvars:Constrintern.ltac_sign ->
-  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  ?ltacvars:ltac_sign ->
+  constr_expr -> evar_map * constr
 val interp_constr :
-  Evd.evar_defs ref ->
-  Environ.env -> Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env -> constr_expr -> evar_map * constr
 val interp_type :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
-  Topconstr.constr_expr -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> evar_map * constr
 val interp_casted_constr :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  ?impls:Constrintern.full_implicits_env ->
-  Topconstr.constr_expr -> Term.types -> Evd.evar_map * Term.constr
+  evar_defs ref ->
+  env ->
+  ?impls:full_implicits_env ->
+  constr_expr -> types -> evar_map * constr
 val interp_open_constr :
-  Evd.evar_defs ref -> Environ.env -> Topconstr.constr_expr -> Term.constr
+  evar_defs ref -> env -> constr_expr -> constr
 val interp_constr_judgment :
-  Evd.evar_defs ref ->
-  Environ.env ->
-  Topconstr.constr_expr -> Evd.evar_defs * Environ.unsafe_judgment
+  evar_defs ref ->
+  env ->
+  constr_expr -> evar_defs * unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
-val collect_non_rec :
-  Environ.env ->
-  Names.identifier list ->
-  ('a * Term.types) list ->
-  'b list ->
-  'c list ->
-  (Names.identifier * ('a * Term.types) * 'b) list *
-  (Names.identifier array * ('a * Term.types) array * 'b array * 'c array)
-val recursive_message : Libnames.global_reference array -> Pp.std_ppcmds
+val recursive_message : global_reference array -> std_ppcmds
 val build_recursive :
-  (Topconstr.fixpoint_expr * Vernacexpr.decl_notation) list -> bool -> unit
+  (fixpoint_expr * decl_notation) list -> bool -> unit
diff --git a/contrib/subtac/subtac_interp_fixpoint.ml b/contrib/subtac/subtac_interp_fixpoint.ml
index c668c3503..3ed5790e3 100644
--- a/contrib/subtac/subtac_interp_fixpoint.ml
+++ b/contrib/subtac/subtac_interp_fixpoint.ml
@@ -183,7 +183,7 @@ let rewrite_cases_aux (loc, po, tml, eqns) =
 		let c' = 
 		  List.fold_left 
 		    (fun acc (n, t) ->
-		       RLambda (dummy_loc, n, t, acc))
+		       RLambda (dummy_loc, n, mkHole, acc))
 		    c eqs_types
 		in (loc, idl, cpl, c'))
       eqns
@@ -204,3 +204,7 @@ let rec rewrite_cases c =
 	   | _ -> assert(false))
     | _ -> map_rawconstr rewrite_cases c
 	  
+let rewrite_cases env c =
+  let c' = rewrite_cases c in
+  let _ = trace (str "Rewrote cases: " ++ spc () ++ my_print_rawconstr env c') in
+    c'
diff --git a/contrib/subtac/subtac_interp_fixpoint.mli b/contrib/subtac/subtac_interp_fixpoint.mli
index 5a84b2773..ef551aa8d 100644
--- a/contrib/subtac/subtac_interp_fixpoint.mli
+++ b/contrib/subtac/subtac_interp_fixpoint.mli
@@ -39,4 +39,5 @@ val rewrite_cases_aux :
   (Util.loc * Names.identifier list * Rawterm.cases_pattern list *
    Rawterm.rawconstr)
   list -> Rawterm.rawconstr
-val rewrite_cases : Rawterm.rawconstr -> Rawterm.rawconstr
+
+val rewrite_cases : Environ.env -> Rawterm.rawconstr -> Rawterm.rawconstr
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 8dd6f9b8f..5cc735185 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -40,8 +40,11 @@ open Context
 open Eterm
 
 module Pretyping = Pretyping.Pretyping_F(Subtac_coercion.Coercion)
+
 open Pretyping
 
+let _ = Pretyping.allow_anonymous_refs := true
+
 type recursion_info = {
   arg_name: name;
   arg_type: types; (* A *)
diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli
index 5bbd4639e..84001c374 100644
--- a/contrib/subtac/subtac_utils.mli
+++ b/contrib/subtac/subtac_utils.mli
@@ -1,53 +1,63 @@
+open Term
+open Libnames
+open Coqlib
+open Environ
+open Pp
+open Evd
+open Decl_kinds
+open Topconstr
+open Rawterm
+open Util
+
 val contrib_name : string
 val subtac_dir : string list
 val fix_sub_module : string
 val fixsub_module : string list
-val init_constant : string list -> string -> Term.constr
-val init_reference : string list -> string -> Libnames.global_reference
-val fixsub : Term.constr lazy_t
-val make_ref : string -> Libnames.reference
-val well_founded_ref : Libnames.reference
-val acc_ref : Libnames.reference
-val acc_inv_ref : Libnames.reference
-val fix_sub_ref : Libnames.reference
-val lt_wf_ref : Libnames.reference
-val sig_ref : Libnames.reference
-val proj1_sig_ref : Libnames.reference
-val proj2_sig_ref : Libnames.reference
-val build_sig : unit -> Coqlib.coq_sigma_data
-val sig_ : Coqlib.coq_sigma_data lazy_t
-val eqind : Term.constr lazy_t
-val eqind_ref : Libnames.global_reference lazy_t
-val refl_equal_ref : Libnames.global_reference lazy_t
-val boolind : Term.constr lazy_t
-val sumboolind : Term.constr lazy_t
-val natind : Term.constr lazy_t
-val intind : Term.constr lazy_t
-val existSind : Term.constr lazy_t
-val existS : Coqlib.coq_sigma_data lazy_t
-val well_founded : Term.constr lazy_t
-val fix : Term.constr lazy_t
-val extconstr : Term.constr -> Topconstr.constr_expr
-val extsort : Term.sorts -> Topconstr.constr_expr
-val my_print_constr : Environ.env -> Term.constr -> Pp.std_ppcmds
-val my_print_context : Environ.env -> Pp.std_ppcmds
-val my_print_env : Environ.env -> Pp.std_ppcmds
-val my_print_rawconstr : Environ.env -> Rawterm.rawconstr -> Pp.std_ppcmds
+val init_constant : string list -> string -> constr
+val init_reference : string list -> string -> global_reference
+val fixsub : constr lazy_t
+val make_ref : string -> reference
+val well_founded_ref : reference
+val acc_ref : reference
+val acc_inv_ref : reference
+val fix_sub_ref : reference
+val lt_wf_ref : reference
+val sig_ref : reference
+val proj1_sig_ref : reference
+val proj2_sig_ref : reference
+val build_sig : unit -> coq_sigma_data
+val sig_ : coq_sigma_data lazy_t
+val eqind : constr lazy_t
+val eqind_ref : global_reference lazy_t
+val refl_equal_ref : global_reference lazy_t
+val boolind : constr lazy_t
+val sumboolind : constr lazy_t
+val natind : constr lazy_t
+val intind : constr lazy_t
+val existSind : constr lazy_t
+val existS : coq_sigma_data lazy_t
+val well_founded : constr lazy_t
+val fix : constr lazy_t
+val extconstr : constr -> constr_expr
+val extsort : sorts -> constr_expr
+val my_print_constr : env -> constr -> std_ppcmds
+val my_print_context : env -> std_ppcmds
+val my_print_env : env -> std_ppcmds
+val my_print_rawconstr : env -> rawconstr -> std_ppcmds
 val debug_level : int ref
-val debug : int -> Pp.std_ppcmds -> unit
-val debug_msg : int -> Pp.std_ppcmds -> Pp.std_ppcmds
-val trace : Pp.std_ppcmds -> unit
-val wf_relations : (Term.constr, Term.constr lazy_t) Hashtbl.t
-val std_relations : unit Lazy.t
-type binders = Topconstr.local_binder list
+val debug : int -> std_ppcmds -> unit
+val debug_msg : int -> std_ppcmds -> std_ppcmds
+val trace : std_ppcmds -> unit
+val wf_relations : (constr, constr lazy_t) Hashtbl.t
+
+type binders = local_binder list
 val app_opt : ('a -> 'a) option -> 'a -> 'a
-val print_args : Environ.env -> Term.constr array -> Pp.std_ppcmds
-val make_existential :
-  Util.loc -> Environ.env -> Evd.evar_defs ref -> Term.types -> Term.constr
-val make_existential_expr : Util.loc -> 'a -> 'b -> Topconstr.constr_expr
-val string_of_hole_kind : Evd.hole_kind -> string
-val non_instanciated_map : Environ.env -> Evd.evar_defs ref -> Evd.evar_map
-val global_kind : Decl_kinds.logical_kind
-val goal_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind
-val global_fix_kind : Decl_kinds.logical_kind
-val goal_fix_kind : Decl_kinds.locality_flag * Decl_kinds.goal_object_kind
+val print_args : env -> constr array -> std_ppcmds
+val make_existential : loc -> env -> evar_defs ref -> types -> constr
+val make_existential_expr : loc -> 'a -> 'b -> constr_expr
+val string_of_hole_kind : hole_kind -> string
+val non_instanciated_map : env -> evar_defs ref -> evar_map
+val global_kind : logical_kind
+val goal_kind : locality_flag * goal_object_kind
+val global_fix_kind : logical_kind
+val goal_fix_kind : locality_flag * goal_object_kind
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 14326bf44..68342e706 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -63,6 +63,9 @@ sig
 
   module Cases : Cases.S
   
+  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+  val allow_anonymous_refs : bool ref
+
   (* Generic call to the interpreter from rawconstr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)
@@ -134,6 +137,9 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 
   module Cases = Cases.Cases_F(Coercion)
 
+  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+  let allow_anonymous_refs = ref false
+
   let evd_comb0 f isevars =
     let (evd',x) = f !isevars in
       isevars := evd';
@@ -422,8 +428,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
               (List.rev nal) cs.cs_args in
 	    let env_f = push_rels fsign env in
 	      (* Make dependencies from arity signature impossible *)
-	    let arsgn,_ = get_arity env indf in
-	    let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+	    let arsgn =
+	      let arsgn,_ = get_arity env indf in
+		if not !allow_anonymous_refs then
+		  List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn
+		else arsgn
+	    in
 	    let psign = (na,None,build_dependent_inductive env indf)::arsgn in
 	    let nar = List.length arsgn in
 	      (match po with
@@ -477,9 +487,13 @@ module Pretyping_F (Coercion : Coercion.S) = struct
             user_err_loc (loc,"",
 			  str "If is only for inductive types with two constructors");
 
-	  (* Make dependencies from arity signature impossible *)
-	  let arsgn,_ = get_arity env indf in
-	  let arsgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn in
+	  let arsgn = 
+	    let arsgn,_ = get_arity env indf in
+	      if not !allow_anonymous_refs then
+		(* Make dependencies from arity signature impossible *)
+		List.map (fun (_,b,t) -> (Anonymous,b,t)) arsgn 
+	      else arsgn
+	  in
 	  let nar = List.length arsgn in
 	  let psign = (na,None,build_dependent_inductive env indf)::arsgn in
 	  let pred,p = match po with
@@ -500,7 +514,17 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	    let n = rel_context_length cs.cs_args in
 	    let pi = liftn n 2 pred in
 	    let pi = beta_applist (pi, [build_dependent_constructor cs]) in
-	    let csgn = List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args in
+	    let csgn = 
+	      if not !allow_anonymous_refs then
+		List.map (fun (_,b,t) -> (Anonymous,b,t)) cs.cs_args 
+	      else 
+		List.map 
+		  (fun (n, b, t) ->
+		     match n with
+                         Name _ -> (n, b, t)
+                       | Anonymous -> (Name (id_of_string "H"), b, t))
+		cs.cs_args
+	    in
 	    let env_c = push_rels csgn env in 
 	    let bj = pretype (Some pi) env_c isevars lvar b in
 	      it_mkLambda_or_LetIn bj.uj_val cs.cs_args in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index f93e46129..ac8e6fec7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -27,7 +27,10 @@ module type S =
 sig
 
   module Cases : Cases.S
-  
+    
+  (* Allow references to syntaxically inexistent variables (i.e., if applied on an inductive) *)
+  val allow_anonymous_refs : bool ref
+
   (* Generic call to the interpreter from rawconstr to open_constr, leaving
      unresolved holes as evars and returning the typing contexts of
      these evars. Work as [understand_gen] for the rest. *)