diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-26 01:09:11 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:43 +0100 |
| commit | 8beca748d992cd08e2dd7448c8b28dadbcea4a16 (patch) | |
| tree | 2cb484e735e9a138991e4cd1e540c6de879e67f6 /pretyping/find_subterm.ml | |
| parent | e1010899051546467b790bca0409174bde824270 (diff) | |
Cleaning up interfaces.
We make mli files look to what they were looking before the move to EConstr
by opening this module.
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 15409f2b8..d09686f6e 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -141,8 +141,8 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = let replace_term_occ_modulo evd occs test bywhat t = let occs',like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in - EConstr.Unsafe.to_constr (proceed_with_occurrences - (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t) + proceed_with_occurrences + (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t let replace_term_occ_decl_modulo evd occs test bywhat d = let (plocs,hyploc),like_first = |