HUGE COMMIT

1. when applying a functor F(X) := B to a module M, the obtained module
   is no longer B{X.t := M.t for all t}, but B{X.t := b where b is the
   body of t in M}. In principle it is now easy to fine tune the behaviour
   to choose whether b or M.t must be used. This change implies modifications
   both inside and outside the kernel.
2. for each object in the library it is now necessary to define the behaviour
   w.r.t. the substitution {X.t := b}. Notice that in many many cases the
   pre-existing behaviour w.r.t. the substitution {X.t := M.t} was broken
   (in the sense that it used to break several invariants). This commit
   fixes the behaviours for most of the objects, excluded
     a) coercions: a future commit should allow any term to be declared
        as a coercion; moreover the invariant that just a coercion path
        exists between two classes will be broken by the instantiation.
     b) global references when used as arguments of a few tactics/commands
   In all the other cases the behaviour implemented is the one that looks
   to me as the one expected by the user (if possible):
   [ terminology: not expanded (X.t := M.t) vs expanded (X.t := b) ]
     a) argument scopes: not expanded
     b) SYNTAXCONSTANT: expanded
     c) implicit arguments: not expanded
     d) coercions: expansion to be done (for now not expanded)
     e) concrete syntax tree for patterns: expanded
     f) concrete syntax tree for raw terms: expanded
     g) evaluable references (used by unfold, delta expansion, etc.): not
        expanded
     h) auto's hints: expanded when possible (i.e. when the expansion of the
        head of the pattern is rigid)
     i) realizers (for program extraction): nothing is done since the actual
        code does not look for the realizer of definitions with a body;
        however this solution is fragile.
     l) syntax and notation: expanded
     m) structures and canonical structures: an invariant says that no
        parameter can happear in them ==> the substitution always yelds the
        original term
     n) stuff related to V7 syntax: since this part of the code is doomed
        to disappear, I have made no effort to fix a reasonable semantics;
        not expanded is the default one applied
     o) RefArgTypes: to be understood. For now a warning is issued whether
        expanded != not expanded, and the not expanded solution is chosen.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6555 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 33 insertions, 15 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index fedf91d534..4ac300827e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -305,7 +305,10 @@ let subst_autohint (_,subst,(local,name,hintlist as obj)) =
     }
   in
   let subst_hint (lab,data as hint) =
-    let lab' = subst_global subst lab in
+    let lab',elab' = subst_global subst lab in
+    let lab' =
+     try head_of_constr_reference (List.hd (head_constr_bound elab' []))
+     with Tactics.Bound -> lab' in
     let data' = match data.code with
       | Res_pf (c, clenv) ->
 	  let c' = subst_mps subst c in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index edf99f175d..4068289eb9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -14,6 +14,7 @@ open Pp
 open Pcoq
 open Genarg
 open Extraargs
+open Mod_subst
 
 (* Equality *)
 open Equality
@@ -348,7 +349,7 @@ let step left x tac =
   let l =
     List.map (fun lem ->
       tclTHENLAST
-      (apply_with_bindings (constr_of_reference lem, ImplicitBindings [x]))
+      (apply_with_bindings (lem, ImplicitBindings [x]))
         tac)
       !(if left then transitivity_left_table else transitivity_right_table)
   in
@@ -362,7 +363,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
   else
     transitivity_right_table := lem :: !transitivity_right_table
   
-let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_global subst ref)
+let subst_transitivity_lemma (_,subst,(b,ref)) = (b,subst_mps subst ref)
 
 let (inTransitivity,_) =
   declare_object {(default_object "TRANSITIVITY-STEPS") with
@@ -394,8 +395,9 @@ let _ =
 
 (* Main entry points *)
 
-let add_transitivity_lemma left ref =
-  add_anonymous_leaf (inTransitivity (left,Nametab.global ref))
+let add_transitivity_lemma left lem =
+ let lem' = Constrintern.interp_constr Evd.empty (Global.env ()) lem in
+  add_anonymous_leaf (inTransitivity (left,lem'))
 
 (* Vernacular syntax *)
 
@@ -410,11 +412,11 @@ TACTIC EXTEND Stepr
 END
 
 VERNAC COMMAND EXTEND AddStepl
-| [ "Declare" "Left" "Step" global(id) ] ->
-    [ add_transitivity_lemma true id ]
+| [ "Declare" "Left" "Step" constr(t) ] ->
+    [ add_transitivity_lemma true t ]
 END
 
 VERNAC COMMAND EXTEND AddStepr
-| [ "Declare" "Right" "Step" global(id) ] ->
-    [ add_transitivity_lemma false id ]
+| [ "Declare" "Right" "Step" constr(t) ] ->
+    [ add_transitivity_lemma false t ]
 END
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8eb7982125..2c9b053ddd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -42,6 +42,7 @@ open Hiddentac
 open Genarg
 open Decl_kinds
 open Mod_subst
+open Printer
 
 let strip_meta id = (* For Grammar v7 compatibility *)
   let s = string_of_id id in
@@ -116,8 +117,8 @@ let pr_value env = function
   | VVoid -> str "()"
   | VInteger n -> int n
   | VIntroPattern ipat -> pr_intro_pattern ipat
-  | VConstr c -> Printer.prterm_env env c
-  | VConstr_context c -> Printer.prterm_env env c
+  | VConstr c -> prterm_env env c
+  | VConstr_context c -> prterm_env env c
   | (VTactic _ | VRTactic _ | VFun _ | VRec _) -> str "<fun>"
 
 (* Transforms a named_context into a (string * constr) list *)
@@ -236,7 +237,7 @@ let coerce_to_inductive = function
 	  | VConstr c -> reference_of_constr c
 	  | _ -> failwith "" in
 	errorlabstrm "coerce_to_inductive"
-          (Printer.pr_global r ++ str " is not an inductive type")
+          (pr_global r ++ str " is not an inductive type")
       with _ ->
 	errorlabstrm "coerce_to_inductive"
           (str "Found an argument which should be an inductive type")
@@ -1841,7 +1842,7 @@ let subst_inductive subst (kn,i) = (subst_kn subst kn,i)
 
 let subst_rawconstr subst (c,e) =
   assert (e=None); (* e<>None only for toplevel tactics *)
-  (subst_raw subst c,None)
+  (Detyping.subst_raw subst c,None)
 
 let subst_binding subst (loc,b,c) =
   (loc,subst_quantified_hypothesis subst b,subst_rawconstr subst c)
@@ -1872,11 +1873,23 @@ let subst_located f (_loc,id) = (loc,f id)
 let subst_reference subst = 
   subst_or_var (subst_located (subst_kn subst))
 
+(*CSC: subst_global_reference is used "only" for RefArgType, that propagates
+  to the syntactic non-terminals "global", used in commands such as
+  Print. It is also used for non-evaluable references. *) 
 let subst_global_reference subst = 
-  subst_or_var (subst_located (subst_global subst))
+ let subst_global ref =
+  let ref',t' = subst_global subst ref in
+   if not (eq_constr (constr_of_reference ref') t') then
+    ppnl (str "Warning: the reference " ++ pr_global ref ++ str " is not " ++
+          str " expanded to \"" ++ prterm t' ++ str "\", but to " ++
+          pr_global ref') ;
+   ref'
+ in
+  subst_or_var (subst_located subst_global)
 
 let subst_evaluable subst =
-  subst_or_var (subst_and_short_name (subst_evaluable_reference subst))
+  let subst_eval_ref = subst_evaluable_reference subst in
+    subst_or_var (subst_and_short_name subst_eval_ref)
 
 let subst_unfold subst (l,e) = 
   (l,subst_evaluable subst e)