diff options
| author | corbinea | 2003-03-31 11:57:52 +0000 |
|---|---|---|
| committer | corbinea | 2003-03-31 11:57:52 +0000 |
| commit | d8da8cb7b9af7df65f63af30bfa5775531426165 (patch) | |
| tree | 869c7417522fda3f075402aa44199edc20f17ad2 /contrib/funind | |
| parent | 516a349d32dde37d8382df89733662a4e1ad9576 (diff) | |
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3815 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index f99b548ee1..d90b064193 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -66,22 +66,12 @@ let prNamedLConstr s lc = prNamedLConstr_aux lc end - -(* tire de const\_omega.ml *) -let constant dir s = - try - Declare.global_absolute_reference - (Libnames.make_path - (Names.make_dirpath (List.map Names.id_of_string (List.rev dir))) - (Names.id_of_string s)) - with e -> print_endline (String.concat "." dir); print_endline s; - raise e -(* fin const\_omega.ml *) +let constant =Coqlib.gen_constant "Funind" let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) let mkRefl typ c1 = - mkApp ((constant ["Coq"; "Init"; "Logic"] "refl_equal"), + mkApp ((constant ["Init"; "Logic"] "refl_equal"), [| typ; c1|]) let rec popn i c = if i<=0 then c else pop (popn (i-1) c) @@ -183,7 +173,7 @@ let nth_dep_constructor indtype n = build_dependent_constructor cstr_sum, cstr_sum.cs_nargs -let coq_refl_equal = lazy(constant ["Coq"; "Init"; "Logic"] "refl_equal") +let coq_refl_equal = lazy(constant ["Init"; "Logic"] "refl_equal") let rec buildrefl_from_eqs eqs = match eqs with |