aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/search.ml')
-rw-r--r--toplevel/search.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml
index abb0af108..e01978dc1 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -93,10 +93,6 @@ let rec head c =
| LetIn (_,_,_,c) -> head c
| _ -> c
-let constr_to_full_path c = match kind_of_term c with
- | Const sp -> sp
- | _ -> raise No_full_path
-
let xor a b = (a or b) & (not (a & b))
let plain_display ref a c =