Add a boolean to indicate the unfolding state of a primitive projection,

so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.

5 files changed, 12 insertions, 12 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6fa4342d34..564e111e04 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -198,7 +198,7 @@ let strip_params env c =
 	(match cb.Declarations.const_proj with
 	| Some pb -> 
 	  let n = pb.Declarations.proj_npars in
-	    mkApp (mkProj (p, args.(n)), 
+	    mkApp (mkProj (Projection.make p false, args.(n)), 
 		   Array.sub args (n+1) (Array.length args - (n + 1)))
 	| None -> c)
     | _ -> c)
@@ -585,7 +585,7 @@ let make_exact_entry env sigma pri poly ?(name=PathAny) (c, cty, ctx) =
     match kind_of_term cty with
     | Prod _ -> failwith "make_exact_entry"
     | _ ->
-	let pat = snd (Patternops.pattern_of_constr sigma cty) in
+	let pat = snd (Patternops.pattern_of_constr env sigma cty) in
 	let hd =
 	  try head_pattern_bound pat
 	  with BoundPattern -> failwith "make_exact_entry"
@@ -604,7 +604,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
         let sigma' = Evd.merge_context_set univ_flexible dummy_goal.sigma ctx in
         let ce = mk_clenv_from { dummy_goal with sigma = sigma' } (c,cty) in
 	let c' = clenv_type (* ~reduce:false *) ce in
-	let pat = snd (Patternops.pattern_of_constr sigma c') in
+	let pat = snd (Patternops.pattern_of_constr env sigma c') in
         let hd =
 	  try head_pattern_bound pat
           with BoundPattern -> failwith "make_apply_entry" in
@@ -701,7 +701,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
   let ce = mk_clenv_from dummy_goal (c,t) in
   (Some hd, { pri=1;
 	      poly = poly;
-              pat = Some (snd (Patternops.pattern_of_constr sigma (clenv_type ce)));
+              pat = Some (snd (Patternops.pattern_of_constr env sigma (clenv_type ce)));
 	      name = name;
               code=Res_pf_THEN_trivial_fail(c,t,ctx) })
   
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index 5fbc6f5b23..ef813744e2 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -33,7 +33,7 @@ type 'res lookup_res = 'res Dn.lookup_res = Label of 'res | Nothing | Everything
 let decomp_pat =
   let rec decrec acc = function
     | PApp (f,args) -> decrec (Array.to_list args @ acc) f
-    | PProj (p, c) -> (PRef (ConstRef p), c :: acc)
+    | PProj (p, c) -> (PRef (ConstRef (Projection.constant p)), c :: acc)
     | c -> (c,acc)
   in
   decrec []
@@ -41,7 +41,7 @@ let decomp_pat =
 let decomp =
   let rec decrec acc c = match kind_of_term c with
     | App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
-    | Proj (p, c) -> (mkConst p, c :: acc)
+    | Proj (p, c) -> (mkConst (Projection.constant p), c :: acc)
     | Cast (c1,_,_) -> decrec acc c1
     | _ -> (c,acc)
   in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index e25a862ddb..991eac57ed 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -584,7 +584,7 @@ let interp_pure_open_constr ist =
 let interp_typed_pattern ist env sigma (c,_) =
   let sigma, c =
     interp_gen WithoutTypeConstraint ist true pure_open_constr_flags env sigma c in
-  pattern_of_constr sigma c
+  pattern_of_constr env sigma c
 
 (* Interprets a constr expression casted by the current goal *)
 let pf_interp_casted_constr ist gl c =
@@ -986,7 +986,7 @@ let eval_pattern lfun ist env sigma (_,pat as c) =
   if use_types then
     snd (interp_typed_pattern ist env sigma c)
   else
-    instantiate_pattern sigma lfun pat
+    instantiate_pattern env sigma lfun pat
 
 let read_pattern lfun ist env sigma = function
   | Subterm (b,ido,c) -> Subterm (b,ido,eval_pattern lfun ist env sigma c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 23b6498093..69a72db4f7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -124,7 +124,7 @@ let head_constr_bound t =
   let hd,args = decompose_app ccl in
   match kind_of_term hd with
     | Const _ | Ind _ | Construct _ | Var _ -> hd
-    | Proj (p, _) -> mkConst p
+    | Proj (p, _) -> mkConst (Projection.constant p)
     | _ -> raise Bound
 
 let head_constr c =
@@ -139,7 +139,7 @@ let decompose_app_bound t =
     | Ind (i,u) -> IndRef i, args
     | Construct (c,u) -> ConstructRef c, args
     | Var id -> VarRef id, args
-    | Proj (p, c) -> ConstRef p, Array.cons c args
+    | Proj (p, c) -> ConstRef (Projection.constant p), Array.cons c args
     | _ -> raise Bound
 
 (******************************************)
@@ -1172,7 +1172,7 @@ let make_projection env sigma params cstr sign elim i n c u =
 	  let args = extended_rel_vect 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
-	      mkProj (proj, mkApp (c, args))
+	      mkProj (Projection.make proj false, mkApp (c, args))
 	    else
 	      mkApp (mkConstU (proj,u), Array.append (Array.of_list params)
 		[|mkApp (c, args)|])
diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml
index f8d7a197be..9826ecdff6 100644
--- a/tactics/term_dnet.ml
+++ b/tactics/term_dnet.ml
@@ -288,7 +288,7 @@ struct
       Array.fold_left (fun c a -> Term (DApp (c,a)))
         (pat_of_constr f) (Array.map pat_of_constr ca)
     | Proj (p,c) -> 
-        Term (DApp (Term (DRef (ConstRef p)), pat_of_constr c))
+        Term (DApp (Term (DRef (ConstRef (Projection.constant p))), pat_of_constr c))
 
     and ctx_of_constr ctx c = match kind_of_term c with
     | Prod (_,t,c)   -> ctx_of_constr (Term(DCons((pat_of_constr t,None),ctx))) c