diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-19 17:35:03 +0000 |
| commit | 1abd56dea147493178a582569f50c9c6f03c6008 (patch) | |
| tree | 940ad7cdc5bef6de02ea76d7b7bd450920313798 /contrib/interface/dad.ml | |
| parent | 4f17ea4dcc68bb4619dbf2b8578333288f145fe5 (diff) | |
Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern
Utilisation d'ident plutôt que int pour PMeta/CPatVar
Ajout CEvar pour la saisie des Evar
Pas d'entrée utilisateur pour les Meta noyau
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/dad.ml')
| -rw-r--r-- | contrib/interface/dad.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml index 3eb6e7993..a391abf33 100644 --- a/contrib/interface/dad.ml +++ b/contrib/interface/dad.ml @@ -69,8 +69,8 @@ let rec get_subterm (depth:int) (path: int list) (constr:constr) = transform constr terms into abstract syntax trees. The second argument is the substitution, a list of pairs linking an integer and a constr term. *) -let rec map_subst (env :env) (subst:(int * Term.constr) list) = function - | CMeta (_,i) -> +let rec map_subst (env :env) (subst:patvar_map) = function + | CPatVar (_,(_,i)) -> let constr = List.assoc i subst in extern_constr false env constr | x -> map_constr_expr_with_binders (map_subst env) (fun _ x -> x) subst x;; @@ -173,7 +173,7 @@ let dad_rule_names () = List.map (function (s,_) -> s) !dad_rule_list;; (* this function is inspired from matches_core in pattern.ml *) -let constrain ((n : int),(pat : constr_pattern)) sigma = +let constrain ((n : patvar),(pat : constr_pattern)) sigma = if List.mem_assoc n sigma then if pat = (List.assoc n sigma) then sigma else failwith "internal" @@ -248,7 +248,7 @@ let rec sort_list = function [] -> [] | a::l -> add_in_list_sorting a (sort_list l);; -let mk_dad_meta n = CMeta (zz,n);; +let mk_dad_meta n = CPatVar (zz,(true,Nameops.make_ident "DAD" (Some n)));; let mk_rewrite lr ast = let b = in_gen rawwit_bool lr in let cb = in_gen rawwit_constr_with_bindings ((*Ctast.ct_to_ast*) ast,NoBindings) in |