diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 11:37:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-11-29 11:37:43 +0000 |
| commit | b47b104bb33a11f8e880b145f1294e010a96de57 (patch) | |
| tree | 25f9874474172d6b291773e1fabdb064c69711c9 /contrib | |
| parent | d2acf8ee9c2e0dd3904d5d2cf1afd3293fc58b4c (diff) | |
Nouveau long long avec Coq en tête
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1020 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/quote.ml | 2 | ||||
| -rw-r--r-- | contrib/ring/ring.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index a8250f490..666d15dee 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -114,7 +114,7 @@ open Proof_type let constant dir s = Declare.global_absolute_reference - (make_path ("ring"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"ring"::dir) (id_of_string s) CCI) let coq_Empty_vm = lazy (constant ["Quote"] "Empty_vm") let coq_Node_vm = lazy (constant ["Quote"] "Node_vm") diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml index fccdc3e78..aa7b305c0 100644 --- a/contrib/ring/ring.ml +++ b/contrib/ring/ring.ml @@ -27,7 +27,7 @@ let constr_of com = Astterm.interp_constr mt_evd (Global.env()) com let constant dir s = Declare.global_absolute_reference - (make_path ("ring"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"ring"::dir) (id_of_string s) CCI) (* Ring_theory *) @@ -87,7 +87,7 @@ let coq_apolynomial_normalize_ok = let logic_constant dir s = Declare.global_absolute_reference - (make_path ("Init"::dir) (id_of_string s) CCI) + (make_path ("Coq"::"Init"::dir) (id_of_string s) CCI) (* Logic *) let coq_f_equal2 = lazy (logic_constant ["Logic"] "f_equal2") |