From 2fd40ff72d3b7b54422b9b00b394c9c446cb5cd7 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 27 Jun 2013 23:04:06 +0000
Subject: Removed the distinction between generic Ltac vars and Let/Intro
 bindings, which permits using only one environment for interning terms.

Ltac semantics was sligthly changed, as it required introducing
a lot of additional coercions from goal variables to other types.
Ltac seemed to be quite non-uniform, as it tried to represent
hypotheses with intropatterns, instead of the dedicated var type.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16612 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/taccoerce.ml | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'tactics/taccoerce.ml')

diff --git a/tactics/taccoerce.ml b/tactics/taccoerce.ml
index 0d1a48f50..9318955df 100644
--- a/tactics/taccoerce.ml
+++ b/tactics/taccoerce.ml
@@ -88,6 +88,8 @@ let coerce_to_ident fresh env v =
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroIdentifier id -> id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    out_gen (topwit wit_var) v
   else match Value.to_constr v with
   | None -> fail ()
   | Some c ->
@@ -100,6 +102,9 @@ let coerce_to_intro_pattern env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     snd (out_gen (topwit wit_intro_pattern) v)
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    IntroIdentifier id
   else match Value.to_constr v with
   | Some c when isVar c ->
       (* This happens e.g. in definitions like "Tac H = clear H; intro H" *)
@@ -134,6 +139,9 @@ let coerce_to_constr env v =
     ([], c)
   else if has_type v (topwit wit_constr_under_binders) then
     out_gen (topwit wit_constr_under_binders) v
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    (try [], constr_of_id env id with Not_found -> fail ())
   else fail ()
 
 let coerce_to_closed_constr env v =
@@ -146,8 +154,12 @@ let coerce_to_evaluable_ref env v =
   let v = Value.normalize v in
   if has_type v (topwit wit_intro_pattern) then
     match out_gen (topwit wit_intro_pattern) v with
-    | _, IntroIdentifier id when List.mem id (Termops.ids_of_context env) -> EvalVarRef id
+    | _, IntroIdentifier id when is_variable env id -> EvalVarRef id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    if List.mem id (Termops.ids_of_context env) then EvalVarRef id
+    else fail ()
   else
     let ev = match Value.to_constr v with
     | Some c when isConst c -> EvalConstRef (destConst c)
@@ -178,6 +190,9 @@ let coerce_to_hyp env v =
     match out_gen (topwit wit_intro_pattern) v with
     | _, IntroIdentifier id when is_variable env id -> id
     | _ -> fail ()
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    if is_variable env id then id else fail ()
   else match Value.to_constr v with
   | Some c when isVar c -> destVar c
   | _ -> fail ()
@@ -215,6 +230,9 @@ let coerce_to_quantified_hypothesis v =
     match v with
     | _, IntroIdentifier id -> NamedHyp id
     | _ -> raise (CannotCoerceTo "a quantified hypothesis")
+  else if has_type v (topwit wit_var) then
+    let id = out_gen (topwit wit_var) v in
+    NamedHyp id
   else if has_type v (topwit wit_int) then
     AnonHyp (out_gen (topwit wit_int) v)
   else raise (CannotCoerceTo "a quantified hypothesis")
-- 
cgit v1.2.3