Remove dynamic stuff from constr_expr and glob_constr

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

17 files changed, 15 insertions, 59 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index eb817ce1b..8469d6db5 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -741,8 +741,6 @@ let rec extern inctx scopes vars r =
   | GCast (loc,c, CastCoerce) ->
       CCast (loc,sub_extern true scopes vars c, CastCoerce)
 
-  | GDynamic (loc,d) -> CDynamic (loc,d)
-
 and extern_typ (_,scopes) =
   extern true (Some Notation.type_scope,scopes)
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 7cca7347b..7db10d81c 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1351,8 +1351,6 @@ let internalize sigma globalenv env allow_patvar lvar c =
     | CCast (loc, c1, CastCoerce) ->
 	GCast (loc,intern env c1, CastCoerce)
 
-    | CDynamic (loc,d) -> GDynamic (loc,d)
-
   and intern_type env = intern (set_type_scope env)
 
   and intern_local_binder env bind =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index bc067a2f5..a104cd5db 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -182,7 +182,7 @@ let generalizable_vars_of_glob_constr ?(bound=Idset.empty) ?(allowed=Idset.empty
 	array_fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bound vs c in
 	(match k with CastConv (_,t) -> vars bound v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bound vs (loc,idl,p,c) =
     let bound' = List.fold_right Idset.add idl bound  in
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 73fb3452b..839a90da0 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -200,9 +200,9 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
   | GSort (_,s1), GSort (_,s2) -> s1 = s2
   | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when na1 = na2 ->
       on_true_do (f b1 b2 & f c1 c2) add na1
-  | (GCases _ | GRec _ | GDynamic _
+  | (GCases _ | GRec _
     | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_
-  | _,(GCases _ | GRec _ | GDynamic _
+  | _,(GCases _ | GRec _
       | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _)
       -> error "Unsupported construction in recursive notations."
   | (GRef _ | GVar _ | GApp _ | GLambda _ | GProd _
@@ -321,7 +321,7 @@ let aconstr_and_vars_of_glob_constr a =
   | GHole (_,w) -> AHole w
   | GRef (_,r) -> ARef r
   | GPatVar (_,(_,n)) -> APatVar n
-  | GDynamic _ | GEvar _ ->
+  | GEvar _ ->
       error "Existential variables not allowed in notations."
 
   in
@@ -728,7 +728,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
        [(Name id',Explicit,None,GHole(dummy_loc,Evd.BinderType (Name id')))])
        (mkGApp dummy_loc b1 (GVar (dummy_loc,id'))) b2
 
-  | (GDynamic _ | GRec _ | GEvar _), _
+  | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
 
 and match_in u = match_ true u
@@ -870,7 +870,6 @@ type constr_expr =
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
-  | CDynamic of loc * Dyn.t
 
 and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
@@ -936,7 +935,6 @@ let constr_loc = function
   | CGeneralization (loc,_,_,_) -> loc
   | CPrim (loc,_) -> loc
   | CDelimiters (loc,_,_) -> loc
-  | CDynamic _ -> dummy_loc
 
 let cases_pattern_expr_loc = function
   | CPatAlias (loc,_,_) -> loc
@@ -1032,7 +1030,7 @@ let fold_constr_expr_with_binders g f n acc = function
       List.fold_left (fun acc bl -> fold_local_binders g f n acc (CHole (dummy_loc,None)) bl) acc bll
   | CGeneralization (_,_,_,c) -> f n acc c
   | CDelimiters (loc,_,a) -> f n acc a
-  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CDynamic _  | CRef _ ->
+  | CHole _ | CEvar _ | CPatVar _ | CSort _ | CPrim _ | CRef _ ->
       acc
   | CRecord (loc,_,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
@@ -1190,7 +1188,7 @@ let map_constr_expr_with_binders g f e = function
   | CGeneralization (loc,b,a,c) -> CGeneralization (loc,b,a,f e c)
   | CDelimiters (loc,s,a) -> CDelimiters (loc,s,f e a)
   | CHole _ | CEvar _ | CPatVar _ | CSort _
-  | CPrim _ | CDynamic _ | CRef _ as x -> x
+  | CPrim _ | CRef _ as x -> x
   | CRecord (loc,p,l) -> CRecord (loc,p,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
       (* TODO: apply g on the binding variables in pat... *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index ecffed6a4..4527dc48a 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -165,7 +165,6 @@ type constr_expr =
   | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
   | CPrim of loc * prim_token
   | CDelimiters of loc * string * constr_expr
-  | CDynamic of loc * Dyn.t
 
 and fix_expr =
     identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index c0d031709..4970ca131 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -532,7 +532,6 @@ let pr pr sep inherited a =
   | CGeneralization (_,bk,ak,c) -> pr_generalization bk ak (pr mt lsimple c), latom
   | CPrim (_,p) -> pr_prim_token p, prec_of_prim_token p
   | CDelimiters (_,sc,a) -> pr_delimiters sc (pr mt lsimple a), 1
-  | CDynamic _ -> str "<dynamic>", latom
   in
   let loc = constr_loc a in
   pr_with_comments loc
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8dfc201d7..c88c66693 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -585,7 +585,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 		*)
 		let f_res = build_entry_lc env funnames args_res.to_avoid f in
 		combine_results combine_app f_res  args_res
-	    | GDynamic _ ->error "Not handled GDynamic"
 	    | GCast(_,b,_) ->
 		(* for an applied cast we just trash the cast part
 		   and restart the work.
@@ -698,7 +697,6 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
     | GRec _ -> error "Not handled GRec"
     | GCast(_,b,_) ->
 	build_entry_lc env funnames  avoid b
-    | GDynamic _ -> error "Not handled GDynamic"
 and build_entry_lc_from_case env funname make_discr
     (el:tomatch_tuples)
     (brl:Glob_term.cases_clauses) avoid :
@@ -1213,7 +1211,7 @@ let rec compute_cst_params relnames params = function
 		 discriminitation ones *)
   | GSort _ -> params
   | GHole _ -> params
-  | GIf _ | GRec _ | GCast _ | GDynamic _  ->
+  | GIf _ | GRec _ | GCast _ ->
       raise (UserError("compute_cst_params", str "Not handled case"))
 and compute_cst_params_from_app acc (params,rtl) =
   match params,rtl with
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 0de1104e7..cdd0eaf71 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -183,7 +183,6 @@ let change_vars =
 	  GCast(loc,change_vars mapping b, CastConv (k,change_vars mapping t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,change_vars mapping b,CastCoerce)
-      | GDynamic _ -> error "Not handled GDynamic"
   and change_vars_br mapping ((loc,idl,patl,res) as br) =
     let new_mapping = List.fold_right Idmap.remove idl mapping in
     if idmap_is_empty new_mapping
@@ -364,7 +363,6 @@ let rec alpha_rt excluded rt =
 	GCast(loc,alpha_rt excluded b,CastConv(k,alpha_rt excluded t))
     | GCast (loc,b,CastCoerce) ->
 	GCast(loc,alpha_rt excluded b,CastCoerce)
-    | GDynamic _ -> error "Not handled GDynamic"
     | GApp(loc,f,args) ->
 	GApp(loc,
 	     alpha_rt excluded f,
@@ -414,7 +412,6 @@ let is_free_in id =
     | GHole _ -> false
     | GCast (_,b,CastConv (_,t)) -> is_free_in b || is_free_in t
     | GCast (_,b,CastCoerce) -> is_free_in b
-    | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and is_free_in_br (_,ids,_,rt) =
     (not (List.mem id ids)) && is_free_in rt
   in
@@ -513,7 +510,6 @@ let replace_var_by_term x_id term =
 	  GCast(loc,replace_var_by_pattern b,CastConv(k,replace_var_by_pattern t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,replace_var_by_pattern b,CastCoerce)
-      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and replace_var_by_pattern_br ((loc,idl,patl,res) as br) =
     if List.exists (fun id -> id_ord id x_id == 0) idl
     then br
@@ -604,7 +600,7 @@ let ids_of_glob_constr c =
       | GCases (loc,sty,rtntypopt,tml,brchl) ->
 	  List.flatten (List.map (fun (_,idl,patl,c) -> idl @ ids_of_glob_constr [] c) brchl)
       | GRec _ -> failwith "Fix inside a constructor branch"
-      | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> []
+      | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> []
   in
   (* build the set *)
   List.fold_left (fun acc x -> Idset.add x acc) Idset.empty (ids_of_glob_constr [] c)
@@ -668,7 +664,6 @@ let zeta_normalize =
 	  GCast(loc,zeta_normalize_term b,CastConv(k,zeta_normalize_term t))
       | GCast(loc,b,CastCoerce) ->
 	  GCast(loc,zeta_normalize_term b,CastCoerce)
-      | GDynamic _ -> raise (UserError("",str "Not handled GDynamic"))
   and zeta_normalize_br (loc,idl,patl,res) =
     (loc,idl,patl,zeta_normalize_term res)
   in
@@ -706,7 +701,6 @@ let expand_as =
 	  GIf(loc,expand_as map e,(na,Option.map (expand_as map) po),
 	      expand_as map br1, expand_as map br2)
       | GRec _ ->  error "Not handled GRec"
-      | GDynamic _ -> error "Not handled GDynamic"
       | GCast(loc,b,CastConv(kind,t)) -> GCast(loc,expand_as map b,CastConv(kind,expand_as map t))
       | GCast(loc,b,CastCoerce) -> GCast(loc,expand_as map b,CastCoerce)
       | GCases(loc,sty,po,el,brl) ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 1ce6564c1..8caeca57a 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -189,7 +189,7 @@ let rec is_rec names =
   let check_id id names =  Idset.mem id names in
   let rec lookup names = function
     | GVar(_,id) -> check_id id names
-    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ | GDynamic _ -> false
+    | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GCast(_,b,_) -> lookup names b
     | GRec _ -> error "GRec not handled"
     | GIf(_,b,_,lhs,rhs) ->
@@ -764,7 +764,6 @@ let rec add_args id new_args b =
   | CGeneralization _ -> anomaly "add_args : CGeneralization"
   | CPrim _ -> b
   | CDelimiters _ -> anomaly "add_args : CDelimiters"
-  | CDynamic _ -> anomaly "add_args : CDynamic"
 exception Stop of  Topconstr.constr_expr
 
 
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index a842f36eb..d300a71cc 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -558,15 +558,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	in
 	  inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | GDynamic (loc,d) ->
-	if (Dyn.tag d) = "constr" then
-	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env !evdref c) in
-	    j
-	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
-	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
     | GHole loc ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index fd85d15f7..bb1ced154 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -669,7 +669,6 @@ let rec subst_glob_constr subst raw =
 	 | CastCoerce ->
 	     let r1' = subst_glob_constr subst r1 in
 	       if r1' == r1 then raw else GCast (loc,r1',k))
-  | GDynamic _ -> raw
 
 (* Utilities to transform kernel cases to simple pattern-matching problem *)
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 85dcf291c..a4113671f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -67,7 +67,6 @@ type glob_constr =
   | GSort of loc * glob_sort
   | GHole of (loc * hole_kind)
   | GCast of loc * glob_constr * glob_constr cast_type
-  | GDynamic of loc * Dyn.t
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
 
@@ -144,7 +143,7 @@ let map_glob_constr_left_to_right f = function
       let comp1 = f c in
       let comp2 = match k with CastConv (k,t) -> CastConv (k, f t) | x -> x in
       GCast (loc,comp1,comp2)
-  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) as x -> x
+  | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x
 
 let map_glob_constr = map_glob_constr_left_to_right
 
@@ -183,7 +182,6 @@ let map_glob_constr_with_binders_loc loc g f e = function
   | GRef (_,x) -> GRef (loc,x)
   | GEvar (_,x,l) -> GEvar (loc,x,l)
   | GPatVar (_,x) -> GPatVar (loc,x)
-  | GDynamic (_,x) -> GDynamic (loc,x)
 *)
 
 let fold_glob_constr f acc =
@@ -206,7 +204,7 @@ let fold_glob_constr f acc =
 	    fold (Option.fold_left fold acc bbd) bty)) acc bl in
 	Array.fold_left fold (Array.fold_left fold acc tyl) bv
     | GCast (_,c,k) -> fold (match k with CastConv (_, t) -> fold acc t | CastCoerce -> acc) c
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> acc
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc
 
   and fold_pattern acc (_,idl,p,c) = fold acc c
 
@@ -245,7 +243,7 @@ let occur_glob_constr id =
           occur_fix bl)
           idl bl tyl bv)
     | GCast (loc,c,k) -> (occur c) or (match k with CastConv (_, t) -> occur t | CastCoerce -> false)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> false
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> false
 
   and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
 
@@ -303,7 +301,7 @@ let free_glob_vars  =
 	array_fold_left_i vars_fix vs idl
     | GCast (loc,c,k) -> let v = vars bounded vs c in
 	(match k with CastConv (_,t) -> vars bounded v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _ | GDynamic _) -> vs
+    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
 
   and vars_pattern bounded vs (loc,idl,p,c) =
     let bounded' = List.fold_right Idset.add idl bounded  in
@@ -336,7 +334,6 @@ let loc_of_glob_constr = function
   | GSort (loc,_) -> loc
   | GHole (loc,_) -> loc
   | GCast (loc,_,_) -> loc
-  | GDynamic (loc,_) -> loc
 
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index c445bcd24..7fb995a88 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -71,7 +71,6 @@ type glob_constr =
   | GSort of loc * glob_sort
   | GHole of (loc * Evd.hole_kind)
   | GCast of loc * glob_constr * glob_constr cast_type
-  | GDynamic of loc * Dyn.t
 
 and glob_decl = name * binding_kind * glob_constr option * glob_constr
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 978feec7c..901936f33 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -679,15 +679,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  { uj_val = v; uj_type = tval }
 	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
-    | GDynamic (loc,d) ->
-	if (Dyn.tag d) = "constr" then
-	  let c = constr_out d in
-	  let j = (Retyping.get_judgment_of env !evdref c) in
-	    j
-	      (*inh_conv_coerce_to_tycon loc env evdref j tycon*)
-	else
-	  user_err_loc (loc,"pretype",(str "Not a constr tagged Dynamic."))
-
   (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
   and pretype_type valcon env evdref lvar = function
     | GHole loc ->
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a88c5f79b..b310dd645 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -154,9 +154,6 @@ let valueOut = function
   | ast ->
     anomalylabstrm "valueOut" (str "Not a Dynamic ast: ")
 
-(* To embed constr *)
-let constrIn t = CDynamic (dummy_loc,constr_in t)
-
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
 let atomic_mactab = ref Idmap.empty
 let add_primitive_tactic s tac =
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 85fcb7e56..6d7909b3b 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -49,7 +49,6 @@ val tactic_out : Dyn.t -> (interp_sign -> glob_tactic_expr)
 val tacticIn : (interp_sign -> raw_tactic_expr) -> raw_tactic_expr
 val globTacticIn : (interp_sign -> glob_tactic_expr) -> raw_tactic_expr
 val valueIn : value -> raw_tactic_arg
-val constrIn : constr -> constr_expr
 
 (** Sets the debugger mode *)
 val set_debug : debug_info -> unit
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 67f54b523..3fd114afe 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -167,7 +167,7 @@ let rec uri_of_constr c =
       error "Whelp does not support pattern-matching and (co-)fixpoint."
   | GVar _ | GRef _ | GHole _ | GEvar _ | GSort _ | GCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
-  | GPatVar _ | GDynamic _ ->
+  | GPatVar _ ->
       anomaly "Found constructors not supported in constr") ()
 
 let make_string f x = Buffer.reset b; f x; Buffer.contents b