Referring to evars by names. Added a parser for evars (but parsing of

instances still to do). Using heuristics to name after the quantifier
name it comes. Also added a "sigma" to almost all printing functions.

10 files changed, 28 insertions, 24 deletions

diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index e0aee15e6..541b59920 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -316,7 +316,7 @@ let rec match_aliases names constr = function
       let args,bnames,body = match_aliases qnames body q in
 	st::args,bnames,body
 
-let detype_ground c = Detyping.detype false [] [] c
+let detype_ground c = Detyping.detype false [] [] Evd.empty c
 
 let interp_cases info sigma env params (pat:cases_pattern_expr) hyps =
   let et,pinfo =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index b5566127f..c5a474d39 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -1034,12 +1034,12 @@ let thesis_for obj typ per_info env=
   let ind,u = destInd cind in
   let _ = if not (eq_ind ind per_info.per_ind) then
     errorlabstrm "thesis_for"
-      ((Printer.pr_constr_env env obj) ++ spc () ++
+      ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str"cannot give an induction hypothesis (wrong inductive type).") in
   let params,args = List.chop per_info.per_nparams all_args in
   let _ = if not (List.for_all2 eq_constr params per_info.per_params) then
     errorlabstrm "thesis_for"
-      ((Printer.pr_constr_env env obj) ++ spc () ++
+      ((Printer.pr_constr_env env Evd.empty obj) ++ spc () ++
 	 str "cannot give an induction hypothesis (wrong parameters).") in
   let hd2 = (applist ((lift (List.length rc) per_info.per_pred),args@[obj])) in
     compose_prod rc (Reductionops.whd_beta Evd.empty hd2)
@@ -1273,7 +1273,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls =
 let understand_my_constr c gls =
   let env = pf_env gls in
   let nc = names_of_rel_context env in
-  let rawc = Detyping.detype false [] nc c in
+  let rawc = Detyping.detype false [] nc Evd.empty c in
   let rec frob = function
     | GEvar _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark Evar_kinds.Expand,None)
     | rc ->  map_glob_constr frob rc
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index a930245b6..9d909fda3 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -26,8 +26,8 @@ let pr_goal gs =
   let preamb,thesis,penv,pc =
     (str "     *** Declarative Mode ***" ++ fnl ()++fnl ()),
     (str "thesis := "  ++ fnl ()),
-    Printer.pr_context_of env,
-    Printer.pr_goal_concl_style_env env (Goal.V82.concl sigma g)
+    Printer.pr_context_of env sigma,
+    Printer.pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g)
   in
     preamb ++
     str"  " ++ hv 0 (penv ++ fnl () ++
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml
index 7f63c4200..be2e44cff 100644
--- a/plugins/decl_mode/ppdecl_proof.ml
+++ b/plugins/decl_mode/ppdecl_proof.ml
@@ -20,6 +20,8 @@ let pr_label = function
     Anonymous -> mt ()
   | Name id -> pr_id id ++ spc () ++ str ":" ++ spc ()
 
+let pr_constr env c = pr_constr env Evd.empty c
+
 let pr_justification_items env = function
     Some [] -> mt ()
   | Some (_::_ as l) ->
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 076107450..6fd934654 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -118,7 +118,7 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
 	(Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in
   let nt=it_mkLambda_or_LetIn revt (aux m []) in
-  let rawt=Detyping.detype false [] [] nt in
+  let rawt=Detyping.detype false [] [] evmap nt in
   let rec raux n t=
     if Int.equal n 0 then t else
       match t with
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 43bb6dbbf..afa178832 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -231,7 +231,7 @@ let extend_with_auto_hints l seq gl=
 
 let print_cmap map=
   let print_entry c l s=
-    let xc=Constrextern.extern_constr false (Global.env ()) c in
+    let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty c in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index aba93de47..700f67a74 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -599,7 +599,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
 	       | App(f,[| _;_;args2 |]) -> args2
 	       | _ ->
 		   observe (str "cannot compute new term value : " ++ pr_gls g' ++ fnl () ++ str "last hyp is" ++
-			      pr_lconstr_env (pf_env g') new_term_value_eq
+			      pr_lconstr_env (pf_env g') Evd.empty new_term_value_eq
 			   );
 		   anomaly (Pp.str "cannot compute new term value")
 	   in
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 587af35ac..36942636f 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -340,7 +340,7 @@ let raw_push_named (na,raw_value,raw_typ) env =
 
 let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
-    observe (str "new rel env := " ++ Printer.pr_rel_context_of env);
+    observe (str "new rel env := " ++ Printer.pr_rel_context_of env Evd.empty);
 
     match pat with
       | PatVar(_,na) -> Environ.push_rel (na,None,typ) env
@@ -376,7 +376,7 @@ let add_pat_variables pat typ env : Environ.env =
 	~init:(env,[])
     )
   in
-  observe (str "new var env := " ++ Printer.pr_named_context_of res);
+  observe (str "new var env := " ++ Printer.pr_named_context_of res Evd.empty);
   res
 
 
@@ -405,7 +405,7 @@ let rec pattern_to_term_and_type env typ  = function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) csta.(i))
+	     (fun i -> Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty csta.(i))
 	  )
       in
       let patl_as_term =
@@ -488,7 +488,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand Evd.empty env rt in
 		let rt_typ = Typing.type_of env Evd.empty rt_as_constr in
-		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) rt_typ in
+		let res_raw_type = Detyping.detype false [] (Termops.names_of_rel_context env) Evd.empty rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -743,7 +743,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			in
 			let raw_typ_of_id =
 			  Detyping.detype false []
-			    (Termops.names_of_rel_context env_with_pat_ids) typ_of_id
+			    (Termops.names_of_rel_context env_with_pat_ids) Evd.empty typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
 		     pat_ids
@@ -787,7 +787,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      List.map3
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
-		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_as_constr in
+		 let typ = Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
 		 List.fold_right
 		   (fun id  acc ->
@@ -795,7 +795,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.type_of new_env Evd.empty (mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] (Termops.names_of_rel_context new_env) typ_of_id
+			Detyping.detype false [] (Termops.names_of_rel_context new_env) Evd.empty typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -951,7 +951,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 			    GRef (Loc.ghost,Globnames.IndRef (fst ind),None),
 			    (List.map
 			      (fun p -> Detyping.detype false []
-				 (Termops.names_of_rel_context env)
+				 (Termops.names_of_rel_context env) Evd.empty
 				 p) params)@(Array.to_list
 				      (Array.make
 					 (List.length args' - nparam)
@@ -980,10 +980,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				     | Name id' ->
 					 (id',Detyping.detype false []
 					    (Termops.names_of_rel_context env)
+                                            Evd.empty
 					    arg)::acc
 				 else if isVar var_as_constr
 				 then (destVar var_as_constr,Detyping.detype false []
 					 (Termops.names_of_rel_context env)
+                                         Evd.empty
 					 arg)::acc
 				 else acc
 			      )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 953e1f049..e2273972e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -538,7 +538,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
   let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
   let ((_,_,typel),_,_) = Command.interp_fixpoint fixl ntns in
   let constr_expr_typel = 
-    with_full_print (List.map (Constrextern.extern_constr false (Global.env ()))) typel in 
+    with_full_print (List.map (Constrextern.extern_constr false (Global.env ()) Evd.empty)) typel in
   let fixpoint_exprl_with_new_bl = 
     List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ -> 
      
@@ -768,8 +768,8 @@ let make_graph (f_ref:global_reference) =
 	 let env = Global.env () in
 	 let extern_body,extern_type =
 	   with_full_print (fun () ->
-		(Constrextern.extern_constr false env body,
-		 Constrextern.extern_type false env
+		(Constrextern.extern_constr false env Evd.empty body,
+		 Constrextern.extern_type false env Evd.empty
                    ((*FIXNE*) Typeops.type_of_constant_type env c_body.const_type)
 		)
 	     )
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 0886e7f71..0117adede 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -773,7 +773,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
   let mkrawcor nme avoid typ =
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
-    Detyping.detype false (Id.Set.elements avoid) [] substindtyp in
+    Detyping.detype false (Id.Set.elements avoid) [] Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
@@ -821,11 +821,11 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let typ = glob_constr_to_constr_expr tp in
         LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc)
       [] params in
-  let concl = Constrextern.extern_constr false (Global.env()) concl in
+  let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in
   let arity,_ =
     List.fold_left
       (fun (acc,env) (nm,_,c) ->
-        let typ = Constrextern.extern_constr false env c in
+        let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (nm,None,c) env in
         CProdN (Loc.ghost, [[(Loc.ghost,nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
@@ -854,7 +854,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
 let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
-        let traw = Detyping.detype false [] [] t in
+        let traw = Detyping.detype false [] [] Evd.empty t in
         GProd (Loc.ghost,nme,Explicit,traw,t2)
     | (_,Some _,_) -> assert false