From 817308ab59daa40bef09838cfc3d810863de0e46 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 16:53:39 +0200
Subject: Fixing #4221 (interpreting bound variables using ltac env was
 possibly capturing bound names unexpectingly).

We moved renaming to after finding bindings, i.e. in pretyping
"fun x y => x + y" in an ltac environment where y is ltac-bound to x,
we type the body in environment "x y |-" but build "fun y y => Rel 2 + Rel 1"
(which later on is displayed into "fun y y0 => y + y0").

We renounced to renaming in "match" patterns, which was anyway not
working well, as e.g. in

let x := ipattern:y in (forall z, match z with S x => x | x => x end = 0).

which was producing

forall z : nat, match z with 0 => z | S y => y end = 0

because the names in default branches are treated specifically.

It would be easy to support renaming in match again, by putting the
ltac env in the Cases.pattern_matching_problem state and to rename the
names in "typs" (from build_branch), just before returning them at the
end of the function (and similarly in abstract_predicate for the names
occurring in the return predicate).

However, we rename binders in fix which were not interpreted.

There are some difficulties with evar because we want them defined in
the interpreted env (see comment to ltac_interp_name_env).

fix ltac name
---
 pretyping/pretyping.ml  | 76 ++++++++++++++++++++++++++++++-------------------
 pretyping/pretyping.mli |  4 +--
 2 files changed, 48 insertions(+), 32 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 03fe2122c0..a212735c04 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -270,6 +270,18 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
                            str"It cannot be used in a binder.")
         else n
 
+let ltac_interp_name_env k0 lvar env =
+  (* envhd is the initial part of the env when pretype was called first *)
+  (* (in practice is is probably 0, but we have to grant the
+     specification of pretype which accepts to start with a non empty
+     rel_context) *)
+  (* tail is the part of the env enriched by pretyping *)
+  let n = rel_context_length (rel_context env) - k0 in
+  let ctxt,_ = List.chop n (rel_context env) in
+  let env = pop_rel_context n env in
+  let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in
+  push_rel_context ctxt env
+
 let invert_ltac_bound_name lvar env id0 id =
   let id = Id.Map.find id lvar.ltac_idents in
   try mkRel (pi1 (lookup_rel_id id (rel_context env)))
@@ -289,10 +301,6 @@ let pretype_id pretype loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
-    let id =
-      try Id.Map.find id lvar.ltac_idents
-      with Not_found -> id
-    in
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
@@ -413,10 +421,10 @@ let is_GHole = function
 
 let evars = ref Id.Map.empty
 
-let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
+let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var_map) t =
   let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in
-  let pretype_type = pretype_type resolve_tc in
-  let pretype = pretype resolve_tc in
+  let pretype_type = pretype_type k0 resolve_tc in
+  let pretype = pretype k0 resolve_tc in
   match t with
   | GRef (loc,ref,u) ->
       inh_conv_coerce_to_tycon loc env evdref
@@ -436,12 +444,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         with Not_found ->
           user_err_loc (loc,"",str "Unknown existential variable.") in
       let hyps = evar_filtered_context (Evd.find !evdref evk) in
-      let args = pretype_instance resolve_tc env evdref lvar loc hyps evk inst in
+      let args = pretype_instance k0 resolve_tc env evdref lvar loc hyps evk inst in
       let c = mkEvar (evk, args) in
       let j = (Retyping.get_judgment_of env !evdref c) in
 	inh_conv_coerce_to_tycon loc env evdref j tycon
 
   | GPatVar (loc,(someta,n)) ->
+    let env = ltac_interp_name_env k0 lvar env in
     let ty =
       match tycon with
       | Some ty -> ty
@@ -450,6 +459,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty }
 
   | GHole (loc, k, naming, None) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -458,6 +468,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         { uj_val = e_new_evar env evdref ~src:(loc,k) ~naming ty; uj_type = ty }
 
   | GHole (loc, k, _naming, Some arg) ->
+      let env = ltac_interp_name_env k0 lvar env in
       let ty =
         match tycon with
         | Some ty -> ty
@@ -474,12 +485,14 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       | (na,bk,None,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let dcl = (na,None,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl
+        let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
         let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl in
+        let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in
+	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in
     let ctxtv = Array.map (type_bl env empty_rel_context) bl in
     let larj =
       Array.map2
@@ -647,9 +660,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let var = (name,None,j.utj_val) in
     let j' = pretype rng (push_rel var env) evdref lvar c2 in
+    let name = ltac_interp_name lvar name in
     let resj = judge_of_abstraction env (orelse_name name name') j j' in
       inh_conv_coerce_to_tycon loc env evdref resj tycon
 
@@ -658,7 +671,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let j' = match name with
       | Anonymous ->
         let j = pretype_type empty_valcon env evdref lvar c2 in
@@ -668,6 +680,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
         let env' = push_rel_assum var env in
           pretype_type empty_valcon env' evdref lvar c2
     in
+    let name = ltac_interp_name lvar name in
     let resj =
       try
         judge_of_product env name j j'
@@ -689,10 +702,10 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     (* The name specified by ltac is used also to create bindings. So
        the substitution must also be applied on variables before they are
        looked up in the rel context. *)
-    let name = ltac_interp_name lvar name in
     let var = (name,Some j.uj_val,t) in
     let tycon = lift_tycon 1 tycon in
     let j' = pretype tycon (push_rel var env) evdref lvar c2 in
+    let name = ltac_interp_name lvar name in
       { uj_val = mkLetIn (name, j.uj_val, t, j'.uj_val) ;
 	uj_type = subst1 j.uj_val j'.uj_type }
 
@@ -712,8 +725,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
     if not (Int.equal (List.length nal) cs.cs_nargs) then
       user_err_loc (loc,"", str "Destructing let on this type expects " ++ 
 	int cs.cs_nargs ++ str " variables.");
-    let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
-    let na = ltac_interp_name lvar na in
     let fsign, record = 
       match get_projections env indf with
       | None -> List.map2 (fun na (_,c,t) -> (na,c,t))
@@ -729,10 +740,12 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	    (na, c, t) :: aux (n+1) k names l
 	  | [], [] -> []
 	  | _ -> assert false
-	in aux 1 1 (List.rev nal) cs.cs_args, true
-    in
+	in aux 1 1 (List.rev nal) cs.cs_args, true in
     let obj ind p v f =
       if not record then 
+        let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
+        let nal = List.rev nal in
+        let fsign = List.map2 (fun na (_,b,t) -> (na,b,t)) nal fsign in
 	let f = it_mkLambda_or_LetIn f fsign in
 	let ci = make_case_info env (fst ind) LetStyle in
 	  mkCase (ci, p, cj.uj_val,[|f|]) 
@@ -818,7 +831,9 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	| None ->
 	  let p = match tycon with
 	    | Some ty -> ty
-	    | None -> new_type_evar env evdref loc
+	    | None ->
+              let env = ltac_interp_name_env k0 lvar env in
+              new_type_evar env evdref loc
 	  in
 	    it_mkLambda_or_LetIn (lift (nar+1) p) psign, p in
       let pred = nf_evar !evdref pred in
@@ -854,9 +869,6 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
       inh_conv_coerce_to_tycon loc env evdref cj tycon
 
   | GCases (loc,sty,po,tml,eqns) ->
-    let (tml,eqns) =
-      Glob_ops.map_pattern_binders (fun na -> ltac_interp_name lvar na) tml eqns
-    in
     Cases.compile_cases loc sty
       ((fun vtyc env evdref -> pretype vtyc env evdref lvar),evdref)
       tycon env (* loc *) (po,tml,eqns)
@@ -903,13 +915,13 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 	  { uj_val = v; uj_type = tval }
     in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
+and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   let f (id,_,t) (subst,update) =
     let t = replace_vars subst t in
     let c, update =
       try
         let c = List.assoc id update in
-        let c = pretype resolve_tc (mk_tycon t) env evdref lvar c in
+        let c = pretype k0 resolve_tc (mk_tycon t) env evdref lvar c in
         c.uj_val, List.remove_assoc id update
       with Not_found ->
       try
@@ -929,7 +941,7 @@ and pretype_instance resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type resolve_tc valcon env evdref lvar = function
+and pretype_type k0 resolve_tc valcon env evdref lvar = function
   | GHole (loc, knd, naming, None) ->
       (match valcon with
        | Some v ->
@@ -945,11 +957,12 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 	     { utj_val = v;
 	       utj_type = s }
        | None ->
+           let env = ltac_interp_name_env k0 lvar env in
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
   | c ->
-      let j = pretype resolve_tc empty_tycon env evdref lvar c in
+      let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in
 	match valcon with
@@ -962,13 +975,14 @@ and pretype_type resolve_tc valcon env evdref lvar = function
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let evdref = ref sigma in
+  let k0 = rel_context_length (rel_context env) in
   let c' = match kind with
     | WithoutTypeConstraint ->
-        (pretype flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
+        (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
     | OfType exptyp ->
-	(pretype flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
+	(pretype k0 flags.use_typeclasses (mk_tycon exptyp) env evdref lvar c).uj_val
     | IsType ->
-	(pretype_type flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
+	(pretype_type k0 flags.use_typeclasses empty_valcon env evdref lvar c).utj_val 
   in
   process_inference_flags flags env sigma (!evdref,c')
 
@@ -1003,14 +1017,16 @@ let on_judgment f j =
 
 let understand_judgment env sigma c =
   let evdref = ref sigma in
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
     let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in 
       evdref := evd; c) j
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
-  let j = pretype true empty_tycon env evdref empty_lvar c in
+  let k0 = rel_context_length (rel_context env) in
+  let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
     evdref := evd; c) j
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b54513e..a6aa086579 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -123,11 +123,11 @@ val check_evars_are_solved :
 (**/**)
 (** Internal of Pretyping... *)
 val pretype :
-  bool -> type_constraint -> env -> evar_map ref ->
+  int -> bool -> type_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_judgment
 
 val pretype_type :
-  bool -> val_constraint -> env -> evar_map ref ->
+  int -> bool -> val_constraint -> env -> evar_map ref ->
   ltac_var_map -> glob_constr -> unsafe_type_judgment
 
 val ise_pretype_gen :
-- 
cgit v1.2.3


From 21525bae8801d98ff2f1b52217d7603505ada2d2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:13:05 +0200
Subject: Cosmetic in evarconv.ml: naming a local function for better
 readibility.

---
 pretyping/evarconv.ml | 35 ++++++++++++++++++-----------------
 1 file changed, 18 insertions(+), 17 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index bb07bf0563..4fed09d6f4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -425,8 +425,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
 	    else quick_fail i)
 	  ev lF tM i
-    and consume (termF,skF as apprF) (termM,skM as apprM) i = 
+    and consume (termF,skF as apprF) (termM,skM as apprM) i =
       if not (Stack.is_empty skF && Stack.is_empty skM) then
+        (* This tries first-order matching *)
         consume_stack on_left apprF apprM i
       else quick_fail i
     and delta i =
@@ -469,28 +470,28 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	     | Construct u -> eta_constructor ts env evd skR u skF termF
 	     | _ -> UnifFailure (evd,NotSameHead)
     in
+    let postpone tR lF evd =
+      (* Postpone the use of an heuristic *)
+      if not (occur_rigidly (fst ev) evd tR) then
+        let evd,tF =
+          if isRel tR || isVar tR then
+            (* Optimization so as to generate candidates *)
+            let evd,ev = evar_absorb_arguments env evd ev lF in
+            evd,mkEvar ev
+          else
+            evd,Stack.zip apprF in
+	switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd))
+	  tF tR
+      else
+        UnifFailure (evd,OccurCheck (fst ev,tR))
+    in
     match Stack.list_of_app_stack skF with
     | None ->
         ise_try evd [consume_stack on_left apprF apprR; eta]
     | Some lF ->
         let tR = Stack.zip apprR in
 	  miller_pfenning on_left
-	    (fun () ->
-	      ise_try evd 
-	        [eta;(* Postpone the use of an heuristic *)
-		 (fun i -> 
-		   if not (occur_rigidly (fst ev) i tR) then
-                     let i,tF =
-                       if isRel tR || isVar tR then
-                         (* Optimization so as to generate candidates *)
-                         let i,ev = evar_absorb_arguments env i ev lF in
-                         i,mkEvar ev
-                       else
-                         i,Stack.zip apprF in
-		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
-	               tF tR
-		   else
-                     UnifFailure (evd,OccurCheck (fst ev,tR)))])
+	    (fun () -> ise_try evd [eta;postpone tR lF])
 	    ev lF tR evd
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
-- 
cgit v1.2.3


From 342fed039e53f00ff8758513149f8d41fa3a2e99 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:14:09 +0200
Subject: Evarconv.ml: small cut-elimination, saving useless zip.

---
 pretyping/evarconv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 4fed09d6f4..3f4411c058 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -417,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let not_only_app = Stack.not_purely_applicative skM in
     let f1 i =
       match Stack.list_of_app_stack skF with
-      | None -> default_fail evd
+      | None -> quick_fail evd
       | Some lF -> 
         let tM = Stack.zip apprM in
 	  miller_pfenning on_left
-- 
cgit v1.2.3


From 6737055d165c91904fc04534bee6b9c05c0235b1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Mar 2015 15:35:04 +0200
Subject: Cosmetic changes in evarconv.ml: hopefully using better
 self-documenting names.

---
 pretyping/evarconv.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3f4411c058..3b51cb1feb 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -380,12 +380,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   in
   let consume_stack on_left (termF,skF) (termO,skO) evd =
     let switch f a b = if on_left then f a b else f b a in
-    let not_only_app = Stack.not_purely_applicative skO in
-    match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
-      |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
-      |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
-	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+    let not_only_appO = Stack.not_purely_applicative skO in
+    match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with
+      |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) ->
+        (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
+        (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
+      |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) ->
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
       |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
-- 
cgit v1.2.3


From d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Mar 2015 15:41:46 +0200
Subject: Cosmetic changes in evarconv.ml: hopefully more regular form and
 naming of arguments of eta.

---
 pretyping/evarconv.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 3b51cb1feb..d3e18953a5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -391,15 +391,15 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
       |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
-  let eta env evd onleft sk term sk' term' =
-    assert (match sk with [] -> true | _ -> false);
-    let (na,c1,c'1) = destLambda term in
+  let eta env evd onleft (termR,skR) (termO,skO) =
+    assert (match skR with [] -> true | _ -> false);
+    let (na,c1,c'1) = destLambda termR in
     let c = nf_evar evd c1 in
     let env' = push_rel (na,None,c) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), 
+      (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
       Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
@@ -468,7 +468,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let switch f a b = if on_left then f a b else f b a in
     let eta evd =
              match kind_of_term termR with
-	     | Lambda _ -> eta env evd false skR termR skF termF
+	     | Lambda _ -> eta env evd false apprR apprF
 	     | Construct u -> eta_constructor ts env evd skR u skF termF
 	     | _ -> UnifFailure (evd,NotSameHead)
     in
@@ -712,10 +712,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     (* Eta-expansion *)
     | Rigid, _ when isLambda term1 ->
-        eta env evd true sk1 term1 sk2 term2
+        eta env evd true appr1 appr2
 
     | _, Rigid when isLambda term2 ->
-        eta env evd false sk2 term2 sk1 term1
+        eta env evd false appr2 appr1
 
     | Rigid, Rigid -> begin
         match kind_of_term term1, kind_of_term term2 with
-- 
cgit v1.2.3


From fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Mar 2015 15:43:56 +0200
Subject: Cosmetic changes in evarconv.ml: hopefully more regular names and
 form of arguments of eta_constructor.

---
 pretyping/evarconv.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d3e18953a5..b73ff2bc5d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -469,7 +469,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let eta evd =
              match kind_of_term termR with
 	     | Lambda _ -> eta env evd false apprR apprF
-	     | Construct u -> eta_constructor ts env evd skR u skF termF
+	     | Construct u -> eta_constructor ts env evd (u,skR) apprF
 	     | _ -> UnifFailure (evd,NotSameHead)
     in
     let postpone tR lF evd =
@@ -755,10 +755,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  rigids env evd sk1 term1 sk2 term2
 
 	| Construct u, _ ->
-	  eta_constructor ts env evd sk1 u sk2 term2
+	  eta_constructor ts env evd (u,sk1) appr2
 	    
 	| _, Construct u ->
-	  eta_constructor ts env evd sk2 u sk1 term1
+	  eta_constructor ts env evd (u,sk2) appr1
 
 	| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
 	  if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -854,7 +854,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	 (fst (decompose_app_vect (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
-and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
-- 
cgit v1.2.3


From 7532f3243ba585f21a8f594d3dc788e38dfa2cb8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:28:04 +0200
Subject: Hopefully clearer printing of stack when debugging evarconv
 unification.

---
 pretyping/reductionops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dc70f36ccf..2892de7c45 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -306,7 +306,9 @@ struct
     | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
   and pr pr_c l =
     let open Pp in
-    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
+    str "[" ++
+    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++
+    str "]"
 
   and pr_cst_member pr_c c =
     let open Pp in
-- 
cgit v1.2.3


From 21e41af41b52914469885f40155702f325d5c786 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Jul 2015 21:28:24 +0200
Subject: Documenting in passing.

---
 pretyping/reductionops.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 1df2a73b2e..51df07f286 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -90,6 +90,9 @@ module Stack : sig
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
   val not_purely_applicative : 'a t -> bool
+
+  (** @return the arguments in the stack if a purely applicative
+      stack, None otherwise *)
   val list_of_app_stack : constr t -> constr list option
 
   val assign : 'a t -> int -> 'a -> 'a t
-- 
cgit v1.2.3


From 35ba593b4ecb805b4e69c01c56fb4b93dfafdf0b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 19:31:00 +0200
Subject: Reverting 16 last commits, committed mistakenly using the wrong push
 command. Sorry so much.

Reverted:
707bfd5719b76d131152a258d49740165fbafe03.
164637cc3a4e8895ed4ec420e300bd692d3e7812.
b9c96c601a8366b75ee8b76d3184ee57379e2620.
21e41af41b52914469885f40155702f325d5c786.
7532f3243ba585f21a8f594d3dc788e38dfa2cb8.
27fb880ab6924ec20ce44aeaeb8d89592c1b91cd.
fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c.
d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962.
6737055d165c91904fc04534bee6b9c05c0235b1.
342fed039e53f00ff8758513149f8d41fa3a2e99.
21525bae8801d98ff2f1b52217d7603505ada2d2.
b78d86d50727af61e0c4417cf2ef12cbfc73239d.
979de570714d340aaab7a6e99e08d46aa616e7da.
f556da10a117396c2c796f6915321b67849f65cd.
d8226295e6237a43de33475f798c3c8ac6ac4866.
fdab811e58094accc02875c1f83e6476f4598d26.
---
 pretyping/evarconv.ml      | 73 ++++++++++++++++++++++------------------------
 pretyping/reductionops.ml  |  4 +--
 pretyping/reductionops.mli |  3 --
 3 files changed, 36 insertions(+), 44 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b73ff2bc5d..bb07bf0563 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -380,26 +380,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
   in
   let consume_stack on_left (termF,skF) (termO,skO) evd =
     let switch f a b = if on_left then f a b else f b a in
-    let not_only_appO = Stack.not_purely_applicative skO in
-    match switch (ise_stack2 not_only_appO env evd (evar_conv_x ts)) skF skO with
-      |Some (lF,rO), Success i' when on_left && (not_only_appO || List.is_empty lF) ->
-        (* Case (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
-        (* or (?termF,stk) = (termO,u1..un::stk') with stk,stk' w/o app *)
-	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
-      |Some (rO,lF), Success i' when not on_left && (not_only_appO || List.is_empty lF) ->
-	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,lF)) (Stack.zip(termO,rO))
+    let not_only_app = Stack.not_purely_applicative skO in
+    match switch (ise_stack2 not_only_app env evd (evar_conv_x ts)) skF skO with
+      |Some (l,r), Success i' when on_left && (not_only_app || List.is_empty l) ->
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
+      |Some (r,l), Success i' when not on_left && (not_only_app || List.is_empty l) ->
+	switch (evar_conv_x ts env i' pbty) (Stack.zip(termF,l)) (Stack.zip(termO,r))
       |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termO
       |_, (UnifFailure _ as x) -> x
       |Some _, _ -> UnifFailure (evd,NotSameArgSize) in
-  let eta env evd onleft (termR,skR) (termO,skO) =
-    assert (match skR with [] -> true | _ -> false);
-    let (na,c1,c'1) = destLambda termR in
+  let eta env evd onleft sk term sk' term' =
+    assert (match sk with [] -> true | _ -> false);
+    let (na,c1,c'1) = destLambda term in
     let c = nf_evar evd c1 in
     let env' = push_rel (na,None,c) env in
     let out1 = whd_betaiota_deltazeta_for_iota_state
       (fst ts) env' evd Cst_stack.empty (c'1, Stack.empty) in
     let out2 = whd_nored_state evd
-      (Stack.zip (termO, skO @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty),
+      (Stack.zip (term', sk' @ [Stack.Shift 1]), Stack.append_app [|mkRel 1|] Stack.empty), 
       Cst_stack.empty in
     if onleft then evar_eqappr_x ts env' evd CONV out1 out2
     else evar_eqappr_x ts env' evd CONV out2 out1
@@ -419,7 +417,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let not_only_app = Stack.not_purely_applicative skM in
     let f1 i =
       match Stack.list_of_app_stack skF with
-      | None -> quick_fail evd
+      | None -> default_fail evd
       | Some lF -> 
         let tM = Stack.zip apprM in
 	  miller_pfenning on_left
@@ -427,9 +425,8 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	      switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i)) (Stack.zip apprF) tM
 	    else quick_fail i)
 	  ev lF tM i
-    and consume (termF,skF as apprF) (termM,skM as apprM) i =
+    and consume (termF,skF as apprF) (termM,skM as apprM) i = 
       if not (Stack.is_empty skF && Stack.is_empty skM) then
-        (* This tries first-order matching *)
         consume_stack on_left apprF apprM i
       else quick_fail i
     and delta i =
@@ -468,32 +465,32 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
     let switch f a b = if on_left then f a b else f b a in
     let eta evd =
              match kind_of_term termR with
-	     | Lambda _ -> eta env evd false apprR apprF
-	     | Construct u -> eta_constructor ts env evd (u,skR) apprF
+	     | Lambda _ -> eta env evd false skR termR skF termF
+	     | Construct u -> eta_constructor ts env evd skR u skF termF
 	     | _ -> UnifFailure (evd,NotSameHead)
     in
-    let postpone tR lF evd =
-      (* Postpone the use of an heuristic *)
-      if not (occur_rigidly (fst ev) evd tR) then
-        let evd,tF =
-          if isRel tR || isVar tR then
-            (* Optimization so as to generate candidates *)
-            let evd,ev = evar_absorb_arguments env evd ev lF in
-            evd,mkEvar ev
-          else
-            evd,Stack.zip apprF in
-	switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) evd))
-	  tF tR
-      else
-        UnifFailure (evd,OccurCheck (fst ev,tR))
-    in
     match Stack.list_of_app_stack skF with
     | None ->
         ise_try evd [consume_stack on_left apprF apprR; eta]
     | Some lF ->
         let tR = Stack.zip apprR in
 	  miller_pfenning on_left
-	    (fun () -> ise_try evd [eta;postpone tR lF])
+	    (fun () ->
+	      ise_try evd 
+	        [eta;(* Postpone the use of an heuristic *)
+		 (fun i -> 
+		   if not (occur_rigidly (fst ev) i tR) then
+                     let i,tF =
+                       if isRel tR || isVar tR then
+                         (* Optimization so as to generate candidates *)
+                         let i,ev = evar_absorb_arguments env i ev lF in
+                         i,mkEvar ev
+                       else
+                         i,Stack.zip apprF in
+		     switch (fun x y -> Success (add_conv_pb (pbty,env,x,y) i))
+	               tF tR
+		   else
+                     UnifFailure (evd,OccurCheck (fst ev,tR)))])
 	    ev lF tR evd
   in
   let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
@@ -712,10 +709,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 
     (* Eta-expansion *)
     | Rigid, _ when isLambda term1 ->
-        eta env evd true appr1 appr2
+        eta env evd true sk1 term1 sk2 term2
 
     | _, Rigid when isLambda term2 ->
-        eta env evd false appr2 appr1
+        eta env evd false sk2 term2 sk1 term1
 
     | Rigid, Rigid -> begin
         match kind_of_term term1, kind_of_term term2 with
@@ -755,10 +752,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
 	  rigids env evd sk1 term1 sk2 term2
 
 	| Construct u, _ ->
-	  eta_constructor ts env evd (u,sk1) appr2
+	  eta_constructor ts env evd sk1 u sk2 term2
 	    
 	| _, Construct u ->
-	  eta_constructor ts env evd (u,sk2) appr1
+	  eta_constructor ts env evd sk2 u sk1 term1
 
 	| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
 	  if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -854,7 +851,7 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
 	 (fst (decompose_app_vect (substl ks h))))]
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
-and eta_constructor ts env evd (((ind, i), u),sk1) (term2,sk2) =
+and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
     | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite <> Decl_kinds.CoFinite -> 
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2892de7c45..dc70f36ccf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -306,9 +306,7 @@ struct
     | Update t -> str "ZUpdate(" ++ pr_c t ++ str ")"
   and pr pr_c l =
     let open Pp in
-    str "[" ++
-    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l ++
-    str "]"
+    prlist_with_sep pr_semicolon (fun x -> hov 1 (pr_member pr_c x)) l
 
   and pr_cst_member pr_c c =
     let open Pp in
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 51df07f286..1df2a73b2e 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -90,9 +90,6 @@ module Stack : sig
   val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
 
   val not_purely_applicative : 'a t -> bool
-
-  (** @return the arguments in the stack if a purely applicative
-      stack, None otherwise *)
   val list_of_app_stack : constr t -> constr list option
 
   val assign : 'a t -> int -> 'a -> 'a t
-- 
cgit v1.2.3


From 97fba91264669d495643f6a3de6a09790ae2a1da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Aug 2015 21:08:12 +0200
Subject: Continuing 817308ab (use ltac env for terms in ltac context) + fix of
 syntax in test file ltac.v.

---
 pretyping/pretyping.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a212735c04..2858a5c1fe 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -297,13 +297,14 @@ let protected_get_type_of env sigma c =
       (str "Cannot reinterpret " ++ quote (print_constr c) ++
        str " in the current environment.")
 
-let pretype_id pretype loc env evdref lvar id =
+let pretype_id pretype k0 loc env evdref lvar id =
   let sigma = !evdref in
   (* Look for the binder of [id] *)
   try
     let (n,_,typ) = lookup_rel_id id (rel_context env) in
       { uj_val  = mkRel n; uj_type = lift n typ }
   with Not_found ->
+    let env = ltac_interp_name_env k0 lvar env in
     (* Check if [id] is an ltac variable *)
     try
       let (ids,c) = Id.Map.find id lvar.ltac_constrs in
@@ -433,7 +434,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
 
   | GVar (loc, id) ->
     inh_conv_coerce_to_tycon loc env evdref
-      (pretype_id (fun e r l t -> pretype tycon e r l t) loc env evdref lvar id)
+      (pretype_id (fun e r l t -> pretype tycon e r l t) k0 loc env evdref lvar id)
       tycon
 
   | GEvar (loc, id, inst) ->
-- 
cgit v1.2.3